Anne is cold. Anne is smart. Dave is big. Dave is cold. Dave is rough. Dave is smart. Erin is kind. Erin is rough. Fiona is big. Fiona is cold. Fiona is rough. Cold things are green. All green things are white. All smart things are cold. If Erin is white and Erin is big then Erin is kind. All green things are big. Kind things are white. If something is big then it is rough. White things are green. Big, white things are smart.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Cold things are green.
((("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
All green things are white.
((("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
All smart things are cold.
((("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
If Erin is white and Erin is big then Erin is kind.
((("Erin" "is" "white" "+") ("Erin" "is" "big" "+")) -> ("Erin" "is" "kind" "+"))
All green things are big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
Kind things are white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
If something is big then it is rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
White things are green.
((("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
Big, white things are smart.
((("something" "is" "big" "+") ("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
Fiona is rough.
True
1
proof
[(triple11 OR ((triple9) -> rule7) OR ((((((triple10) -> rule1)) -> rule5)) -> rule7))]
("Fiona" "is" "rough" "+")
triple11
((triple9) -> (rule7 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
((((((triple10) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is not big.
False
1
inv-proof
[(triple9 OR ((((triple10) -> rule1)) -> rule5))]
("Fiona" "is" "big" "-")
triple9
((((triple10) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Anne is green.
True
2
proof
[(((triple1) -> rule1) OR ((((triple2) -> rule3)) -> rule1))]
("Anne" "is" "green" "+")
((triple1) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Fiona is not green.
False
2
inv-proof
[(((triple10) -> rule1))]
("Fiona" "is" "green" "-")
((triple10) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Anne is white.
True
3
proof
[(((((triple1) -> rule1)) -> rule2) OR ((((((triple2) -> rule3)) -> rule1)) -> rule2))]
("Anne" "is" "white" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is not white.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2) OR ((((((triple2) -> rule3)) -> rule1)) -> rule2))]
("Anne" "is" "white" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Erin is big.
True
4
proof
[(((((((triple7) -> rule6)) -> rule8)) -> rule5))]
("Erin" "is" "big" "+")
((((((triple7) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Fiona is not smart.
False
5
inv-proof
[(((triple9 ((((triple10) -> rule1)) -> rule2)) -> rule9) OR ((((((triple10) -> rule1)) -> rule5) ((((triple10) -> rule1)) -> rule2)) -> rule9))]
("Fiona" "is" "smart" "-")
((triple9 ((((triple10) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
((((((triple10) -> (rule1 % int4))) -> (rule5 % int3)) ((((triple10) -> (rule1 % int4))) -> (rule2 % int2))) -> (rule9 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
Erin is smart.
True
7
proof
[(((((((((triple7) -> rule6)) -> rule8)) -> rule5) ((triple7) -> rule6)) -> rule9))]
("Erin" "is" "smart" "+")
((((((((triple7) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule5 % int2)) ((triple7) -> (rule6 % int4))) -> (rule9 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Erin is not smart.
False
7
inv-proof
[(((((((((triple7) -> rule6)) -> rule8)) -> rule5) ((triple7) -> rule6)) -> rule9))]
("Erin" "is" "smart" "-")
((((((((triple7) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule5 % int2)) ((triple7) -> (rule6 % int4))) -> (rule9 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Erin is cold.
True
8
proof
[(((((((((((triple7) -> rule6)) -> rule8)) -> rule5) ((triple7) -> rule6)) -> rule9)) -> rule3))]
("Erin" "is" "cold" "+")
((((((((((triple7) -> (rule6 % int5))) -> (rule8 % int4))) -> (rule5 % int3)) ((triple7) -> (rule6 % int5))) -> (rule9 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
Erin is white.
("Erin" "is" "white" "+")
int5
Erin is not cold.
False
8
inv-proof
[(((((((((((triple7) -> rule6)) -> rule8)) -> rule5) ((triple7) -> rule6)) -> rule9)) -> rule3))]
("Erin" "is" "cold" "-")
((((((((((triple7) -> (rule6 % int5))) -> (rule8 % int4))) -> (rule5 % int3)) ((triple7) -> (rule6 % int5))) -> (rule9 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
Erin is white.
("Erin" "is" "white" "+")
int5
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
@0: Anne is cold.[(triple1 OR ((triple2) -> rule3))] Anne is smart.[(triple2 OR ((((((triple1) -> rule1)) -> rule5) ((((triple1) -> rule1)) -> rule2)) -> rule9))] Dave is big.[(triple3 OR ((((triple4) -> rule1)) -> rule5) OR ((((((triple6) -> rule3)) -> rule1)) -> rule5))] Dave is cold.[(triple4 OR ((triple6) -> rule3))] Dave is rough.[(triple5 OR ((triple3) -> rule7) OR ((((((triple4) -> rule1)) -> rule5)) -> rule7) OR ((((((((triple6) -> rule3)) -> rule1)) -> rule5)) -> rule7))] Dave is smart.[(triple6 OR ((triple3 ((((triple4) -> rule1)) -> rule2)) -> rule9) OR ((((((triple4) -> rule1)) -> rule5) ((((triple4) -> rule1)) -> rule2)) -> rule9))] Erin is kind.[(triple7)] Erin is rough.[(triple8 OR ((((((((triple7) -> rule6)) -> rule8)) -> rule5)) -> rule7))] Fiona is big.[(triple9 OR ((((triple10) -> rule1)) -> rule5))] Fiona is cold.[(triple10)] Fiona is rough.[(triple11 OR ((triple9) -> rule7) OR ((((((triple10) -> rule1)) -> rule5)) -> rule7))] @1: Anne is green.[(((triple1) -> rule1) OR ((((triple2) -> rule3)) -> rule1))] Dave is green.[(((triple4) -> rule1) OR ((((triple6) -> rule3)) -> rule1))] Erin is white.[(((triple7) -> rule6))] Fiona is green.[(((triple10) -> rule1))] @2: Anne is big.[(((((triple1) -> rule1)) -> rule5) OR ((((((triple2) -> rule3)) -> rule1)) -> rule5))] Anne is white.[(((((triple1) -> rule1)) -> rule2) OR ((((((triple2) -> rule3)) -> rule1)) -> rule2))] Dave is white.[(((((triple4) -> rule1)) -> rule2) OR ((((((triple6) -> rule3)) -> rule1)) -> rule2))] Erin is green.[(((((triple7) -> rule6)) -> rule8))] Fiona is white.[(((((triple10) -> rule1)) -> rule2))] @3: Anne is rough.[(((((((triple1) -> rule1)) -> rule5)) -> rule7) OR ((((((((triple2) -> rule3)) -> rule1)) -> rule5)) -> rule7))] Erin is big.[(((((((triple7) -> rule6)) -> rule8)) -> rule5))] Fiona is smart.[(((triple9 ((((triple10) -> rule1)) -> rule2)) -> rule9) OR ((((((triple10) -> rule1)) -> rule5) ((((triple10) -> rule1)) -> rule2)) -> rule9))] @4: Erin is smart.[(((((((((triple7) -> rule6)) -> rule8)) -> rule5) ((triple7) -> rule6)) -> rule9))] @5: Erin is cold.[(((((((((((triple7) -> rule6)) -> rule8)) -> rule5) ((triple7) -> rule6)) -> rule9)) -> rule3))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
((triple2) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
((((((triple1) -> (rule1 % int4))) -> (rule5 % int3)) ((((triple1) -> (rule1 % int4))) -> (rule2 % int2))) -> (rule9 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
Dave is big.
("Dave" "is" "big" "+")
triple3
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((((((triple6) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
triple4
((triple6) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple5
((triple3) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((((triple4) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
((((((((triple6) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
int4
Dave is smart.
("Dave" "is" "smart" "+")
triple6
((triple3 ((((triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
((((((triple4) -> (rule1 % int4))) -> (rule5 % int3)) ((((triple4) -> (rule1 % int4))) -> (rule2 % int2))) -> (rule9 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Erin is kind.
("Erin" "is" "kind" "+")
triple7
Erin is rough.
("Erin" "is" "rough" "+")
triple8
((((((((triple7) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Fiona is big.
("Fiona" "is" "big" "+")
triple9
((((triple10) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
triple10
Fiona is rough.
("Fiona" "is" "rough" "+")
triple11
((triple9) -> (rule7 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
((((((triple10) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((triple4) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
((triple7) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
((triple10) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((((((triple6) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
((((triple7) -> (rule6 % int2))) -> (rule8 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
((((triple10) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
((((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
((((((((triple2) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Erin is big.
("Erin" "is" "big" "+")
((((((triple7) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple9 ((((triple10) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
((((((triple10) -> (rule1 % int4))) -> (rule5 % int3)) ((((triple10) -> (rule1 % int4))) -> (rule2 % int2))) -> (rule9 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
Erin is smart.
("Erin" "is" "smart" "+")
((((((((triple7) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule5 % int2)) ((triple7) -> (rule6 % int4))) -> (rule9 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Erin is cold.
("Erin" "is" "cold" "+")
((((((((((triple7) -> (rule6 % int5))) -> (rule8 % int4))) -> (rule5 % int3)) ((triple7) -> (rule6 % int5))) -> (rule9 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
Erin is white.
("Erin" "is" "white" "+")
int5