Bob is blue. Bob is furry. Bob is rough. Charlie is blue. Charlie is rough. Charlie is smart. Charlie is white. Dave is blue. Dave is green. Dave is rough. Dave is smart. Gary is blue. Gary is furry. Gary is rough. Gary is white. If something is green and smart then it is furry. If something is rough then it is green. If something is smart and young then it is blue. If Charlie is blue then Charlie is smart. If something is smart and furry then it is green. All rough, furry things are young.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is white.
("Gary" "is" "white" "+")
If something is green and smart then it is furry.
((("something" "is" "green" "+") ("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
If something is rough then it is green.
((("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
If something is smart and young then it is blue.
((("something" "is" "smart" "+") ("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
If Charlie is blue then Charlie is smart.
((("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "smart" "+"))
If something is smart and furry then it is green.
((("something" "is" "smart" "+") ("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
All rough, furry things are young.
((("something" "is" "rough" "+") ("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
Charlie is rough.
True
1
proof
[(triple5)]
("Charlie" "is" "rough" "+")
triple5
Charlie is not smart.
False
1
inv-proof
[(triple6 OR ((triple4) -> rule4))]
("Charlie" "is" "smart" "-")
triple6
((triple4) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Bob is green.
True
2
proof
[(((triple3) -> rule2))]
("Bob" "is" "green" "+")
((triple3) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Charlie is not green.
False
2
inv-proof
[(((triple5) -> rule2))]
("Charlie" "is" "green" "-")
((triple5) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Dave is young.
True
5
proof
[(((triple10 ((triple9 triple11) -> rule1)) -> rule6) OR ((triple10 ((((triple10) -> rule2) triple11) -> rule1)) -> rule6))]
("Dave" "is" "young" "+")
((triple10 ((triple9 triple11) -> (rule1 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((triple10 ((((triple10) -> (rule2 % int3)) triple11) -> (rule1 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Charlie is not furry.
False
4
inv-proof
[(((((triple5) -> rule2) triple6) -> rule1) OR ((((triple5) -> rule2) ((triple4) -> rule4)) -> rule1))]
("Charlie" "is" "furry" "-")
((((triple5) -> (rule2 % int2)) triple6) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((((triple5) -> (rule2 % int3)) ((triple4) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Bob is not smart.
Unknown
inv-random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
@0: Bob is blue.[(triple1)] Bob is furry.[(triple2)] Bob is rough.[(triple3)] Charlie is blue.[(triple4 OR ((triple6 ((triple5 ((((triple5) -> rule2) triple6) -> rule1)) -> rule6)) -> rule3))] Charlie is rough.[(triple5)] Charlie is smart.[(triple6 OR ((triple4) -> rule4))] Charlie is white.[(triple7)] Dave is blue.[(triple8 OR ((triple11 ((triple10 ((triple9 triple11) -> rule1)) -> rule6)) -> rule3) OR ((triple11 ((triple10 ((((triple10) -> rule2) triple11) -> rule1)) -> rule6)) -> rule3))] Dave is green.[(triple9 OR ((triple10) -> rule2))] Dave is rough.[(triple10)] Dave is smart.[(triple11)] Gary is blue.[(triple12)] Gary is furry.[(triple13)] Gary is rough.[(triple14)] Gary is white.[(triple15)] @1: Bob is green.[(((triple3) -> rule2))] Bob is young.[(((triple3 triple2) -> rule6))] Charlie is green.[(((triple5) -> rule2))] Dave is furry.[(((triple9 triple11) -> rule1) OR ((((triple10) -> rule2) triple11) -> rule1))] Gary is green.[(((triple14) -> rule2))] Gary is young.[(((triple14 triple13) -> rule6))] @2: Charlie is furry.[(((((triple5) -> rule2) triple6) -> rule1) OR ((((triple5) -> rule2) ((triple4) -> rule4)) -> rule1))] Dave is young.[(((triple10 ((triple9 triple11) -> rule1)) -> rule6) OR ((triple10 ((((triple10) -> rule2) triple11) -> rule1)) -> rule6))] @3: Charlie is young.[(((triple5 ((((triple5) -> rule2) triple6) -> rule1)) -> rule6) OR ((triple5 ((((triple5) -> rule2) ((triple4) -> rule4)) -> rule1)) -> rule6))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is rough.
("Bob" "is" "rough" "+")
triple3
Charlie is blue.
("Charlie" "is" "blue" "+")
triple4
((triple6 ((triple5 ((((triple5) -> (rule2 % int4)) triple6) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
int4
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
((triple4) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
triple7
Dave is blue.
("Dave" "is" "blue" "+")
triple8
((triple11 ((triple10 ((triple9 triple11) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
((triple11 ((triple10 ((((triple10) -> (rule2 % int4)) triple11) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is green.
("Dave" "is" "green" "+")
triple9
((triple10) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple10
Dave is smart.
("Dave" "is" "smart" "+")
triple11
Gary is blue.
("Gary" "is" "blue" "+")
triple12
Gary is furry.
("Gary" "is" "furry" "+")
triple13
Gary is rough.
("Gary" "is" "rough" "+")
triple14
Gary is white.
("Gary" "is" "white" "+")
triple15
Bob is green.
("Bob" "is" "green" "+")
((triple3) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((triple3 triple2) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((triple5) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((triple9 triple11) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((((triple10) -> (rule2 % int2)) triple11) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
((triple14) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple14 triple13) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((((triple5) -> (rule2 % int2)) triple6) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((((triple5) -> (rule2 % int3)) ((triple4) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
((triple10 ((triple9 triple11) -> (rule1 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((triple10 ((((triple10) -> (rule2 % int3)) triple11) -> (rule1 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
((triple5 ((((triple5) -> (rule2 % int3)) triple6) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
((triple5 ((((triple5) -> (rule2 % int4)) ((triple4) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
int4