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