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