Bob is round. Bob is white. Bob is young. Charlie is cold. Fiona is nice. Harry is cold. Harry is round. If something is young then it is round. If something is red then it is nice. All green, cold things are white. Round things are green. If Fiona is round and Fiona is cold then Fiona is young. All red, young things are white. If something is cold and nice then it is young. All white things are red. If Charlie is young and Charlie is cold then Charlie is nice.
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is round.
("Harry" "is" "round" "+")
If something is young then it is round.
((("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
If something is red then it is nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
All green, cold things are white.
((("something" "is" "green" "+") ("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
Round things are green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
If Fiona is round and Fiona is cold then Fiona is young.
((("Fiona" "is" "round" "+") ("Fiona" "is" "cold" "+")) -> ("Fiona" "is" "young" "+"))
All red, young things are white.
((("something" "is" "red" "+") ("something" "is" "young" "+")) -> ("something" "is" "white" "+"))
If something is cold and nice then it is young.
((("something" "is" "cold" "+") ("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
All white things are red.
((("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
If Charlie is young and Charlie is cold then Charlie is nice.
((("Charlie" "is" "young" "+") ("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "nice" "+"))
Charlie is cold.
True
1
proof
[(triple4)]
("Charlie" "is" "cold" "+")
triple4
Harry is not round.
False
1
inv-proof
[(triple7)]
("Harry" "is" "round" "-")
triple7
Bob is red.
True
2
proof
[(((triple2) -> rule8))]
("Bob" "is" "red" "+")
((triple2) -> (rule8 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is not green.
False
2
inv-proof
[(((triple1) -> rule4) OR ((((triple3) -> rule1)) -> rule4))]
("Bob" "is" "green" "-")
((triple1) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Harry is white.
True
4
proof
[(((((triple7) -> rule4) triple6) -> rule3))]
("Harry" "is" "white" "+")
((((triple7) -> (rule4 % int2)) triple6) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is not white.
False
4
inv-proof
[(((((triple7) -> rule4) triple6) -> rule3))]
("Harry" "is" "white" "-")
((((triple7) -> (rule4 % int2)) triple6) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is red.
True
5
proof
[(((((((triple7) -> rule4) triple6) -> rule3)) -> rule8))]
("Harry" "is" "red" "+")
((((((triple7) -> (rule4 % int3)) triple6) -> (rule3 % int2))) -> (rule8 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is not red.
False
5
inv-proof
[(((((((triple7) -> rule4) triple6) -> rule3)) -> rule8))]
("Harry" "is" "red" "-")
((((((triple7) -> (rule4 % int3)) triple6) -> (rule3 % int2))) -> (rule8 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is nice.
True
6
proof
[(((((((((triple7) -> rule4) triple6) -> rule3)) -> rule8)) -> rule2))]
("Harry" "is" "nice" "+")
((((((((triple7) -> (rule4 % int4)) triple6) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
Harry is not nice.
False
6
inv-proof
[(((((((((triple7) -> rule4) triple6) -> rule3)) -> rule8)) -> rule2))]
("Harry" "is" "nice" "-")
((((((((triple7) -> (rule4 % int4)) triple6) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
Harry is young.
True
8
proof
[(((triple6 ((((((((triple7) -> rule4) triple6) -> rule3)) -> rule8)) -> rule2)) -> rule7))]
("Harry" "is" "young" "+")
((triple6 ((((((((triple7) -> (rule4 % int5)) triple6) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
Harry is green.
("Harry" "is" "green" "+")
int5
Harry is not young.
False
8
inv-proof
[(((triple6 ((((((((triple7) -> rule4) triple6) -> rule3)) -> rule8)) -> rule2)) -> rule7))]
("Harry" "is" "young" "-")
((triple6 ((((((((triple7) -> (rule4 % int5)) triple6) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
Harry is green.
("Harry" "is" "green" "+")
int5
Fiona is not round.
Unknown
inv-rconc
[@2: Fiona is round.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Fiona" "is" "round" "-")
Charlie is nice.
Unknown
rconc
[@7: Charlie is nice.[CWA. Example of deepest failure = (rule2 <- rule8 <- rule3 <- rule4 <- rule1 <- rule7 <- rule9 <- FAIL)]]
("Charlie" "is" "nice" "+")
Fiona is not red.
Unknown
inv-rconc
[@2: Fiona is red.[CWA. Example of deepest failure = (rule8 <- rule3 <- FAIL)]]
("Fiona" "is" "red" "-")
Charlie is round.
Unknown
rconc
[@6: Charlie is round.[CWA. Example of deepest failure = (rule1 <- rule7 <- rule2 <- rule8 <- rule3 <- rule4 <- FAIL)]]
("Charlie" "is" "round" "+")
Charlie is not white.
Unknown
inv-rconc
[@7: Charlie is white.[CWA. Example of deepest failure = (rule3 <- rule4 <- rule1 <- rule7 <- rule2 <- rule8 <- rule6 <- FAIL)]]
("Charlie" "is" "white" "-")
Charlie is green.
Unknown
rconc
[@6: Charlie is green.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule7 <- rule2 <- rule8 <- rule3 <- FAIL)]]
("Charlie" "is" "green" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
@0: Bob is round.[(triple1 OR ((triple3) -> rule1))] Bob is white.[(triple2)] Bob is young.[(triple3)] Charlie is cold.[(triple4)] Fiona is nice.[(triple5)] Harry is cold.[(triple6)] Harry is round.[(triple7)] @1: Bob is green.[(((triple1) -> rule4) OR ((((triple3) -> rule1)) -> rule4))] Bob is red.[(((triple2) -> rule8))] Harry is green.[(((triple7) -> rule4))] @2: Bob is nice.[(((((triple2) -> rule8)) -> rule2))] Harry is white.[(((((triple7) -> rule4) triple6) -> rule3))] @3: Harry is red.[(((((((triple7) -> rule4) triple6) -> rule3)) -> rule8))] @4: Harry is nice.[(((((((((triple7) -> rule4) triple6) -> rule3)) -> rule8)) -> rule2))] @5: Harry is young.[(((triple6 ((((((((triple7) -> rule4) triple6) -> rule3)) -> rule8)) -> rule2)) -> rule7))]
Bob is round.
("Bob" "is" "round" "+")
triple1
((triple3) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple3
Charlie is cold.
("Charlie" "is" "cold" "+")
triple4
Fiona is nice.
("Fiona" "is" "nice" "+")
triple5
Harry is cold.
("Harry" "is" "cold" "+")
triple6
Harry is round.
("Harry" "is" "round" "+")
triple7
Bob is green.
("Bob" "is" "green" "+")
((triple1) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
((triple2) -> (rule8 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple7) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((((triple2) -> (rule8 % int2))) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
((((triple7) -> (rule4 % int2)) triple6) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
((((((triple7) -> (rule4 % int3)) triple6) -> (rule3 % int2))) -> (rule8 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
((((((((triple7) -> (rule4 % int4)) triple6) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
Harry is young.
("Harry" "is" "young" "+")
((triple6 ((((((((triple7) -> (rule4 % int5)) triple6) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
Harry is green.
("Harry" "is" "green" "+")
int5