Anne is red. Anne is white. Fiona is smart. Fiona is white. Fiona is young. Harry is blue. Harry is cold. Harry is nice. Harry is red. Harry is smart. Harry is white. Harry is young. White things are young. All smart, white things are young. If Fiona is cold and Fiona is blue then Fiona is white. Cold things are nice. All young things are cold. All smart things are red.
Anne is red.
("Anne" "is" "red" "+")
Anne is white.
("Anne" "is" "white" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
White things are young.
((("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
All smart, white things are young.
((("something" "is" "smart" "+") ("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
If Fiona is cold and Fiona is blue then Fiona is white.
((("Fiona" "is" "cold" "+") ("Fiona" "is" "blue" "+")) -> ("Fiona" "is" "white" "+"))
Cold things are nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
All young things are cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
All smart things are red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
Harry is smart.
True
1
proof
[(triple10)]
("Harry" "is" "smart" "+")
triple10
Fiona is not white.
False
1
inv-proof
[(triple4)]
("Fiona" "is" "white" "-")
triple4
Anne is young.
True
2
proof
[(((triple2) -> rule1))]
("Anne" "is" "young" "+")
((triple2) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Fiona is not red.
False
2
inv-proof
[(((triple3) -> rule6))]
("Fiona" "is" "red" "-")
((triple3) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Anne is cold.
True
3
proof
[(((((triple2) -> rule1)) -> rule5))]
("Anne" "is" "cold" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Fiona is not nice.
False
3
inv-proof
[(((((triple5) -> rule5)) -> rule4) OR ((((((triple4) -> rule1)) -> rule5)) -> rule4) OR ((((((triple3 triple4) -> rule2)) -> rule5)) -> rule4))]
("Fiona" "is" "nice" "-")
((((triple5) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((((((triple4) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
((((((triple3 triple4) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Anne is nice.
True
4
proof
[(((((((triple2) -> rule1)) -> rule5)) -> rule4))]
("Anne" "is" "nice" "+")
((((((triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is not nice.
False
4
inv-proof
[(((((((triple2) -> rule1)) -> rule5)) -> rule4))]
("Anne" "is" "nice" "-")
((((((triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is not smart.
Unknown
inv-random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
@0: Anne is red.[(triple1)] Anne is white.[(triple2)] Fiona is smart.[(triple3)] Fiona is white.[(triple4)] Fiona is young.[(triple5 OR ((triple4) -> rule1) OR ((triple3 triple4) -> rule2))] Harry is blue.[(triple6)] Harry is cold.[(triple7 OR ((triple12) -> rule5) OR ((((triple11) -> rule1)) -> rule5) OR ((((triple10 triple11) -> rule2)) -> rule5))] Harry is nice.[(triple8 OR ((triple7) -> rule4) OR ((((triple12) -> rule5)) -> rule4) OR ((((((triple11) -> rule1)) -> rule5)) -> rule4) OR ((((((triple10 triple11) -> rule2)) -> rule5)) -> rule4))] Harry is red.[(triple9 OR ((triple10) -> rule6))] Harry is smart.[(triple10)] Harry is white.[(triple11)] Harry is young.[(triple12 OR ((triple11) -> rule1) OR ((triple10 triple11) -> rule2))] @1: Anne is young.[(((triple2) -> rule1))] Fiona is cold.[(((triple5) -> rule5) OR ((((triple4) -> rule1)) -> rule5) OR ((((triple3 triple4) -> rule2)) -> rule5))] Fiona is red.[(((triple3) -> rule6))] @2: Anne is cold.[(((((triple2) -> rule1)) -> rule5))] Fiona is nice.[(((((triple5) -> rule5)) -> rule4) OR ((((((triple4) -> rule1)) -> rule5)) -> rule4) OR ((((((triple3 triple4) -> rule2)) -> rule5)) -> rule4))] @3: Anne is nice.[(((((((triple2) -> rule1)) -> rule5)) -> rule4))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Anne is white.
("Anne" "is" "white" "+")
triple2
Fiona is smart.
("Fiona" "is" "smart" "+")
triple3
Fiona is white.
("Fiona" "is" "white" "+")
triple4
Fiona is young.
("Fiona" "is" "young" "+")
triple5
((triple4) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((triple3 triple4) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple6
Harry is cold.
("Harry" "is" "cold" "+")
triple7
((triple12) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((((triple11) -> (rule1 % int2))) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((triple10 triple11) -> (rule2 % int2))) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
triple8
((triple7) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple12) -> (rule5 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((((triple11) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
((((((triple10 triple11) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
triple9
((triple10) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
triple10
Harry is white.
("Harry" "is" "white" "+")
triple11
Harry is young.
("Harry" "is" "young" "+")
triple12
((triple11) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple10 triple11) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((triple2) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple5) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((((triple3 triple4) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
((triple3) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
((((triple5) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((((((triple4) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
((((((triple3 triple4) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
((((((triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3