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