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