Anne is big. Anne is blue. Anne is red. Anne is round. Charlie is quiet. Charlie is red. Charlie is round. Fiona is big. Fiona is blue. Fiona is nice. Fiona is red. Gary is big. Gary is nice. Gary is red. Gary is white. All round, white things are nice. All round things are white. All big things are round.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is white.
("Gary" "is" "white" "+")
All round, white things are nice.
((("something" "is" "round" "+") ("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
All round things are white.
((("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
All big things are round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
Anne is blue.
True
1
proof
[(triple2)]
("Anne" "is" "blue" "+")
triple2
Gary is not nice.
False
1
inv-proof
[(triple13 OR ((((triple12) -> rule3) triple15) -> rule1) OR ((((triple12) -> rule3) ((((triple12) -> rule3)) -> rule2)) -> rule1))]
("Gary" "is" "nice" "-")
triple13
((((triple12) -> (rule3 % int2)) triple15) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((((triple12) -> (rule3 % int3)) ((((triple12) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Charlie is white.
True
2
proof
[(((triple7) -> rule2))]
("Charlie" "is" "white" "+")
((triple7) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Fiona is not round.
False
2
inv-proof
[(((triple8) -> rule3))]
("Fiona" "is" "round" "-")
((triple8) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Anne is nice.
True
4
proof
[(((triple4 ((triple4) -> rule2)) -> rule1) OR ((((triple1) -> rule3) ((triple4) -> rule2)) -> rule1) OR ((triple4 ((((triple1) -> rule3)) -> rule2)) -> rule1) OR ((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule2)) -> rule1))]
("Anne" "is" "nice" "+")
((triple4 ((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((((triple1) -> (rule3 % int3)) ((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
((triple4 ((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Fiona is not white.
False
3
inv-proof
[(((((triple8) -> rule3)) -> rule2))]
("Fiona" "is" "white" "-")
((((triple8) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
@0: Anne is big.[(triple1)] Anne is blue.[(triple2)] Anne is red.[(triple3)] Anne is round.[(triple4 OR ((triple1) -> rule3))] Charlie is quiet.[(triple5)] Charlie is red.[(triple6)] Charlie is round.[(triple7)] Fiona is big.[(triple8)] Fiona is blue.[(triple9)] Fiona is nice.[(triple10 OR ((((triple8) -> rule3) ((((triple8) -> rule3)) -> rule2)) -> rule1))] Fiona is red.[(triple11)] Gary is big.[(triple12)] Gary is nice.[(triple13 OR ((((triple12) -> rule3) triple15) -> rule1) OR ((((triple12) -> rule3) ((((triple12) -> rule3)) -> rule2)) -> rule1))] Gary is red.[(triple14)] Gary is white.[(triple15 OR ((((triple12) -> rule3)) -> rule2))] @1: Anne is white.[(((triple4) -> rule2) OR ((((triple1) -> rule3)) -> rule2))] Charlie is white.[(((triple7) -> rule2))] Fiona is round.[(((triple8) -> rule3))] Gary is round.[(((triple12) -> rule3))] @2: Anne is nice.[(((triple4 ((triple4) -> rule2)) -> rule1) OR ((((triple1) -> rule3) ((triple4) -> rule2)) -> rule1) OR ((triple4 ((((triple1) -> rule3)) -> rule2)) -> rule1) OR ((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule2)) -> rule1))] Charlie is nice.[(((triple7 ((triple7) -> rule2)) -> rule1))] Fiona is white.[(((((triple8) -> rule3)) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
Anne is round.
("Anne" "is" "round" "+")
triple4
((triple1) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple5
Charlie is red.
("Charlie" "is" "red" "+")
triple6
Charlie is round.
("Charlie" "is" "round" "+")
triple7
Fiona is big.
("Fiona" "is" "big" "+")
triple8
Fiona is blue.
("Fiona" "is" "blue" "+")
triple9
Fiona is nice.
("Fiona" "is" "nice" "+")
triple10
((((triple8) -> (rule3 % int3)) ((((triple8) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
triple11
Gary is big.
("Gary" "is" "big" "+")
triple12
Gary is nice.
("Gary" "is" "nice" "+")
triple13
((((triple12) -> (rule3 % int2)) triple15) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((((triple12) -> (rule3 % int3)) ((((triple12) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
triple14
Gary is white.
("Gary" "is" "white" "+")
triple15
((((triple12) -> (rule3 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
((triple4) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((triple7) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
((triple8) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((triple12) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((triple4 ((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((((triple1) -> (rule3 % int3)) ((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
((triple4 ((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple7 ((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
((((triple8) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2