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