Charlie is cold. Charlie is quiet. Charlie is white. Fiona is big. Fiona is blue. Fiona is white. Fiona is young. Gary is cold. Gary is quiet. Gary is round. Harry is quiet. Harry is white. If Charlie is quiet then Charlie is cold. If something is cold and quiet then it is young. All quiet things are cold. Cold, young things are big. If Charlie is round and Charlie is young then Charlie is big. If Fiona is quiet then Fiona is big.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is white.
("Harry" "is" "white" "+")
If Charlie is quiet then Charlie is cold.
((("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "cold" "+"))
If something is cold and quiet then it is young.
((("something" "is" "cold" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
All quiet things are cold.
((("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
Cold, young things are big.
((("something" "is" "cold" "+") ("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
If Charlie is round and Charlie is young then Charlie is big.
((("Charlie" "is" "round" "+") ("Charlie" "is" "young" "+")) -> ("Charlie" "is" "big" "+"))
If Fiona is quiet then Fiona is big.
((("Fiona" "is" "quiet" "+")) -> ("Fiona" "is" "big" "+"))
Harry is white.
True
1
proof
[(triple12)]
("Harry" "is" "white" "+")
triple12
Charlie is not quiet.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "quiet" "-")
triple2
Charlie is young.
True
3
proof
[(((triple1 triple2) -> rule2) OR ((((triple2) -> rule1) triple2) -> rule2) OR ((((triple2) -> rule3) triple2) -> rule2))]
("Charlie" "is" "young" "+")
((triple1 triple2) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple2) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((triple2) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is not young.
False
3
inv-proof
[(((triple1 triple2) -> rule2) OR ((((triple2) -> rule1) triple2) -> rule2) OR ((((triple2) -> rule3) triple2) -> rule2))]
("Charlie" "is" "young" "-")
((triple1 triple2) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple2) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((triple2) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Gary is big.
True
5
proof
[(((triple8 ((triple8 triple9) -> rule2)) -> rule4) OR ((((triple9) -> rule3) ((triple8 triple9) -> rule2)) -> rule4) OR ((triple8 ((((triple9) -> rule3) triple9) -> rule2)) -> rule4) OR ((((triple9) -> rule3) ((((triple9) -> rule3) triple9) -> rule2)) -> rule4))]
("Gary" "is" "big" "+")
((triple8 ((triple8 triple9) -> (rule2 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((((triple9) -> (rule3 % int3)) ((triple8 triple9) -> (rule2 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
((triple8 ((((triple9) -> (rule3 % int3)) triple9) -> (rule2 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
((((triple9) -> (rule3 % int3)) ((((triple9) -> (rule3 % int3)) triple9) -> (rule2 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Charlie is not big.
False
5
inv-proof
[(((triple1 ((triple1 triple2) -> rule2)) -> rule4) OR ((((triple2) -> rule1) ((triple1 triple2) -> rule2)) -> rule4) OR ((((triple2) -> rule3) ((triple1 triple2) -> rule2)) -> rule4) OR ((triple1 ((((triple2) -> rule1) triple2) -> rule2)) -> rule4) OR ((triple1 ((((triple2) -> rule3) triple2) -> rule2)) -> rule4) OR ((((triple2) -> rule1) ((((triple2) -> rule1) triple2) -> rule2)) -> rule4) OR ((((triple2) -> rule1) ((((triple2) -> rule3) triple2) -> rule2)) -> rule4) OR ((((triple2) -> rule3) ((((triple2) -> rule1) triple2) -> rule2)) -> rule4) OR ((((triple2) -> rule3) ((((triple2) -> rule3) triple2) -> rule2)) -> rule4))]
("Charlie" "is" "big" "-")
((triple1 ((triple1 triple2) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
((((triple2) -> (rule1 % int3)) ((triple1 triple2) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
((((triple2) -> (rule3 % int3)) ((triple1 triple2) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
((triple1 ((((triple2) -> (rule1 % int3)) triple2) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
((triple1 ((((triple2) -> (rule3 % int3)) triple2) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
((((triple2) -> (rule1 % int3)) ((((triple2) -> (rule1 % int3)) triple2) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
((((triple2) -> (rule1 % int3)) ((((triple2) -> (rule3 % int3)) triple2) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
((((triple2) -> (rule3 % int3)) ((((triple2) -> (rule1 % int3)) triple2) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
((((triple2) -> (rule3 % int3)) ((((triple2) -> (rule3 % int3)) triple2) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Harry is big.
True
7
proof
[(((((triple11) -> rule3) ((((triple11) -> rule3) triple11) -> rule2)) -> rule4))]
("Harry" "is" "big" "+")
((((triple11) -> (rule3 % int3)) ((((triple11) -> (rule3 % int3)) triple11) -> (rule2 % int2))) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is not big.
False
7
inv-proof
[(((((triple11) -> rule3) ((((triple11) -> rule3) triple11) -> rule2)) -> rule4))]
("Harry" "is" "big" "-")
((((triple11) -> (rule3 % int3)) ((((triple11) -> (rule3 % int3)) triple11) -> (rule2 % int2))) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Fiona is not cold.
Unknown
inv-rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "cold" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
Charlie is not round.
Unknown
inv-random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
@0: Charlie is cold.[(triple1 OR ((triple2) -> rule1) OR ((triple2) -> rule3))] Charlie is quiet.[(triple2)] Charlie is white.[(triple3)] Fiona is big.[(triple4)] Fiona is blue.[(triple5)] Fiona is white.[(triple6)] Fiona is young.[(triple7)] Gary is cold.[(triple8 OR ((triple9) -> rule3))] Gary is quiet.[(triple9)] Gary is round.[(triple10)] Harry is quiet.[(triple11)] Harry is white.[(triple12)] @1: Charlie is young.[(((triple1 triple2) -> rule2) OR ((((triple2) -> rule1) triple2) -> rule2) OR ((((triple2) -> rule3) triple2) -> rule2))] Gary is young.[(((triple8 triple9) -> rule2) OR ((((triple9) -> rule3) triple9) -> rule2))] Harry is cold.[(((triple11) -> rule3))] @2: Charlie is big.[(((triple1 ((triple1 triple2) -> rule2)) -> rule4) OR ((((triple2) -> rule1) ((triple1 triple2) -> rule2)) -> rule4) OR ((((triple2) -> rule3) ((triple1 triple2) -> rule2)) -> rule4) OR ((triple1 ((((triple2) -> rule1) triple2) -> rule2)) -> rule4) OR ((triple1 ((((triple2) -> rule3) triple2) -> rule2)) -> rule4) OR ((((triple2) -> rule1) ((((triple2) -> rule1) triple2) -> rule2)) -> rule4) OR ((((triple2) -> rule1) ((((triple2) -> rule3) triple2) -> rule2)) -> rule4) OR ((((triple2) -> rule3) ((((triple2) -> rule1) triple2) -> rule2)) -> rule4) OR ((((triple2) -> rule3) ((((triple2) -> rule3) triple2) -> rule2)) -> rule4))] Gary is big.[(((triple8 ((triple8 triple9) -> rule2)) -> rule4) OR ((((triple9) -> rule3) ((triple8 triple9) -> rule2)) -> rule4) OR ((triple8 ((((triple9) -> rule3) triple9) -> rule2)) -> rule4) OR ((((triple9) -> rule3) ((((triple9) -> rule3) triple9) -> rule2)) -> rule4))] Harry is young.[(((((triple11) -> rule3) triple11) -> rule2))] @3: Harry is big.[(((((triple11) -> rule3) ((((triple11) -> rule3) triple11) -> rule2)) -> rule4))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
((triple2) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((triple2) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Charlie is white.
("Charlie" "is" "white" "+")
triple3
Fiona is big.
("Fiona" "is" "big" "+")
triple4
Fiona is blue.
("Fiona" "is" "blue" "+")
triple5
Fiona is white.
("Fiona" "is" "white" "+")
triple6
Fiona is young.
("Fiona" "is" "young" "+")
triple7
Gary is cold.
("Gary" "is" "cold" "+")
triple8
((triple9) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
triple9
Gary is round.
("Gary" "is" "round" "+")
triple10
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
Harry is white.
("Harry" "is" "white" "+")
triple12
Charlie is young.
("Charlie" "is" "young" "+")
((triple1 triple2) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple2) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((triple2) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
((triple8 triple9) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((((triple9) -> (rule3 % int2)) triple9) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((triple11) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((triple1 ((triple1 triple2) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
((((triple2) -> (rule1 % int3)) ((triple1 triple2) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
((((triple2) -> (rule3 % int3)) ((triple1 triple2) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
((triple1 ((((triple2) -> (rule1 % int3)) triple2) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
((triple1 ((((triple2) -> (rule3 % int3)) triple2) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
((((triple2) -> (rule1 % int3)) ((((triple2) -> (rule1 % int3)) triple2) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
((((triple2) -> (rule1 % int3)) ((((triple2) -> (rule3 % int3)) triple2) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
((((triple2) -> (rule3 % int3)) ((((triple2) -> (rule1 % int3)) triple2) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
((((triple2) -> (rule3 % int3)) ((((triple2) -> (rule3 % int3)) triple2) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
((triple8 ((triple8 triple9) -> (rule2 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((((triple9) -> (rule3 % int3)) ((triple8 triple9) -> (rule2 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
((triple8 ((((triple9) -> (rule3 % int3)) triple9) -> (rule2 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
((((triple9) -> (rule3 % int3)) ((((triple9) -> (rule3 % int3)) triple9) -> (rule2 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
((((triple11) -> (rule3 % int2)) triple11) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
((((triple11) -> (rule3 % int3)) ((((triple11) -> (rule3 % int3)) triple11) -> (rule2 % int2))) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3