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