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