Bob is blue. Bob is furry. Bob is round. Bob is smart. Bob is white. Dave is furry. Erin is blue. Erin is furry. Erin is green. Erin is round. Erin is white. Harry is smart. All blue things are green. Furry things are blue. If something is round then it is red. Furry, blue things are white. Round things are green. All red things are smart. All smart, green things are round. If something is smart then it is green.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is white.
("Erin" "is" "white" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All blue things are green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
Furry things are blue.
((("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
If something is round then it is red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
Furry, blue things are white.
((("something" "is" "furry" "+") ("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
Round things are green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
All red things are smart.
((("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
All smart, green things are round.
((("something" "is" "smart" "+") ("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
If something is smart then it is green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
Erin is white.
True
1
proof
[(triple11 OR ((triple8 triple7) -> rule4) OR ((triple8 ((triple8) -> rule2)) -> rule4))]
("Erin" "is" "white" "+")
triple11
((triple8 triple7) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple8 ((triple8) -> (rule2 % int2))) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is not blue.
False
1
inv-proof
[(triple7 OR ((triple8) -> rule2))]
("Erin" "is" "blue" "-")
triple7
((triple8) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Harry is green.
True
2
proof
[(((triple12) -> rule8))]
("Harry" "is" "green" "+")
((triple12) -> (rule8 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Erin is not red.
False
2
inv-proof
[(((triple10) -> rule3))]
("Erin" "is" "red" "-")
((triple10) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
True
3
proof
[(((((triple10) -> rule3)) -> rule6))]
("Erin" "is" "smart" "+")
((((triple10) -> (rule3 % int2))) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Dave is not green.
False
3
inv-proof
[(((((triple6) -> rule2)) -> rule1))]
("Dave" "is" "green" "-")
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Harry is red.
True
5
proof
[(((((triple12 ((triple12) -> rule8)) -> rule7)) -> rule3))]
("Harry" "is" "red" "+")
((((triple12 ((triple12) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is not red.
False
5
inv-proof
[(((((triple12 ((triple12) -> rule8)) -> rule7)) -> rule3))]
("Harry" "is" "red" "-")
((((triple12 ((triple12) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Dave is not smart.
Unknown
inv-rconc
[@3: Dave is smart.[CWA. Example of deepest failure = (rule6 <- rule3 <- rule7 <- FAIL)]]
("Dave" "is" "smart" "-")
Dave is red.
Unknown
rconc
[@3: Dave is red.[CWA. Example of deepest failure = (rule3 <- rule7 <- rule6 <- FAIL)]]
("Dave" "is" "red" "+")
Harry is not white.
Unknown
inv-rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "white" "-")
Harry is blue.
Unknown
rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "blue" "+")
@0: Bob is blue.[(triple1 OR ((triple2) -> rule2))] Bob is furry.[(triple2)] Bob is round.[(triple3 OR ((triple4 ((triple1) -> rule1)) -> rule7) OR ((triple4 ((triple4) -> rule8)) -> rule7) OR ((triple4 ((((triple2) -> rule2)) -> rule1)) -> rule7))] Bob is smart.[(triple4 OR ((((triple3) -> rule3)) -> rule6))] Bob is white.[(triple5 OR ((triple2 triple1) -> rule4) OR ((triple2 ((triple2) -> rule2)) -> rule4))] Dave is furry.[(triple6)] Erin is blue.[(triple7 OR ((triple8) -> rule2))] Erin is furry.[(triple8)] Erin is green.[(triple9 OR ((triple10) -> rule5) OR ((triple7) -> rule1) OR ((((triple8) -> rule2)) -> rule1) OR ((((((triple10) -> rule3)) -> rule6)) -> rule8))] Erin is round.[(triple10)] Erin is white.[(triple11 OR ((triple8 triple7) -> rule4) OR ((triple8 ((triple8) -> rule2)) -> rule4))] Harry is smart.[(triple12)] @1: Bob is green.[(((triple1) -> rule1) OR ((triple3) -> rule5) OR ((triple4) -> rule8) OR ((((triple2) -> rule2)) -> rule1) OR ((((((triple3) -> rule3)) -> rule6)) -> rule8))] Bob is red.[(((triple3) -> rule3) OR ((((triple4 ((triple1) -> rule1)) -> rule7)) -> rule3) OR ((((triple4 ((triple4) -> rule8)) -> rule7)) -> rule3) OR ((((triple4 ((((triple2) -> rule2)) -> rule1)) -> rule7)) -> rule3))] Dave is blue.[(((triple6) -> rule2))] Erin is red.[(((triple10) -> rule3))] Harry is green.[(((triple12) -> rule8))] @2: Dave is green.[(((((triple6) -> rule2)) -> rule1))] Dave is white.[(((triple6 ((triple6) -> rule2)) -> rule4))] Erin is smart.[(((((triple10) -> rule3)) -> rule6))] Harry is round.[(((triple12 ((triple12) -> rule8)) -> rule7))] @3: Harry is red.[(((((triple12 ((triple12) -> rule8)) -> rule7)) -> rule3))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
((triple2) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple3
((triple4 ((triple1) -> (rule1 % int2))) -> (rule7 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((triple4 ((triple4) -> (rule8 % int2))) -> (rule7 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((triple4 ((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
triple4
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
triple5
((triple2 triple1) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple2 ((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
triple6
Erin is blue.
("Erin" "is" "blue" "+")
triple7
((triple8) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
triple8
Erin is green.
("Erin" "is" "green" "+")
triple9
((triple10) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((triple7) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
((((((triple10) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
triple10
Erin is white.
("Erin" "is" "white" "+")
triple11
((triple8 triple7) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple8 ((triple8) -> (rule2 % int2))) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
triple12
Bob is green.
("Bob" "is" "green" "+")
((triple1) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((triple3) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((triple4) -> (rule8 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
((triple3) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((((triple4 ((triple1) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
((((triple4 ((triple4) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
((((triple4 ((((triple2) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
Dave is blue.
("Dave" "is" "blue" "+")
((triple6) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((triple10) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple12) -> (rule8 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
((triple6 ((triple6) -> (rule2 % int2))) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
((((triple10) -> (rule3 % int2))) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((triple12 ((triple12) -> (rule8 % int2))) -> (rule7 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
((((triple12 ((triple12) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3