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