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