Bob is big. Bob is furry. Bob is green. Bob is red. Dave is green. Erin is big. Erin is furry. Red, quiet people are big. If someone is big then they are red. If someone is round then they are cold. All furry people are cold. Green, cold people are quiet. All big people are red. Round people are big. All green people are round.
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is red.
("Bob" "is" "red" "+")
Dave is green.
("Dave" "is" "green" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Red, quiet people are big.
((("someone" "is" "red" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
If someone is big then they are red.
((("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
If someone is round then they are cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
All furry people are cold.
((("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
Green, cold people are quiet.
((("someone" "is" "green" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
All big people are red.
((("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
Round people are big.
((("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
All green people are round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
Bob is furry.
True
1
proof
[(triple2)]
("Bob" "is" "furry" "+")
triple2
Dave is not green.
False
1
inv-proof
[(triple5)]
("Dave" "is" "green" "-")
triple5
Erin is red.
True
2
proof
[(((triple6) -> rule2) OR ((triple6) -> rule6))]
("Erin" "is" "red" "+")
((triple6) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((triple6) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Bob is not round.
False
2
inv-proof
[(((triple3) -> rule8))]
("Bob" "is" "round" "-")
((triple3) -> (rule8 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Dave is cold.
True
3
proof
[(((((triple5) -> rule8)) -> rule3))]
("Dave" "is" "cold" "+")
((((triple5) -> (rule8 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not big.
False
3
inv-proof
[(((((triple5) -> rule8)) -> rule7))]
("Dave" "is" "big" "-")
((((triple5) -> (rule8 % int2))) -> (rule7 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is quiet.
True
5
proof
[(((triple5 ((((triple5) -> rule8)) -> rule3)) -> rule5))]
("Dave" "is" "quiet" "+")
((triple5 ((((triple5) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is not red.
False
4
inv-proof
[(((((((triple5) -> rule8)) -> rule7)) -> rule2) OR ((((((triple5) -> rule8)) -> rule7)) -> rule6))]
("Dave" "is" "red" "-")
((((((triple5) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
((((((triple5) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Erin is not round.
Unknown
inv-rconc
[@1: Erin is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Erin" "is" "round" "-")
Erin is quiet.
Unknown
rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "quiet" "+")
Erin is not green.
Unknown
inv-random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
@0: Bob is big.[(triple1 OR ((((triple3) -> rule8)) -> rule7) OR ((triple4 ((triple3 ((triple2) -> rule4)) -> rule5)) -> rule1) OR ((triple4 ((triple3 ((((triple3) -> rule8)) -> rule3)) -> rule5)) -> rule1))] Bob is furry.[(triple2)] Bob is green.[(triple3)] Bob is red.[(triple4 OR ((triple1) -> rule2) OR ((triple1) -> rule6) OR ((((((triple3) -> rule8)) -> rule7)) -> rule2) OR ((((((triple3) -> rule8)) -> rule7)) -> rule6))] Dave is green.[(triple5)] Erin is big.[(triple6)] Erin is furry.[(triple7)] @1: Bob is cold.[(((triple2) -> rule4) OR ((((triple3) -> rule8)) -> rule3))] Bob is round.[(((triple3) -> rule8))] Dave is round.[(((triple5) -> rule8))] Erin is cold.[(((triple7) -> rule4))] Erin is red.[(((triple6) -> rule2) OR ((triple6) -> rule6))] @2: Bob is quiet.[(((triple3 ((triple2) -> rule4)) -> rule5) OR ((triple3 ((((triple3) -> rule8)) -> rule3)) -> rule5))] Dave is big.[(((((triple5) -> rule8)) -> rule7))] Dave is cold.[(((((triple5) -> rule8)) -> rule3))] @3: Dave is quiet.[(((triple5 ((((triple5) -> rule8)) -> rule3)) -> rule5))] Dave is red.[(((((((triple5) -> rule8)) -> rule7)) -> rule2) OR ((((((triple5) -> rule8)) -> rule7)) -> rule6))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((((triple3) -> (rule8 % int2))) -> (rule7 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((triple4 ((triple3 ((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
((triple4 ((triple3 ((((triple3) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
triple4
((triple1) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple1) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((((((triple3) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
((((((triple3) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
triple5
Erin is big.
("Erin" "is" "big" "+")
triple6
Erin is furry.
("Erin" "is" "furry" "+")
triple7
Bob is cold.
("Bob" "is" "cold" "+")
((triple2) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((((triple3) -> (rule8 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
((triple3) -> (rule8 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple5) -> (rule8 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((triple7) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((triple6) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((triple6) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple3 ((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((triple3 ((((triple3) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
((((triple5) -> (rule8 % int2))) -> (rule7 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
((((triple5) -> (rule8 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple5 ((((triple5) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
((((((triple5) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
((((((triple5) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3