Anne is big. Anne is blue. Anne is not nice. Anne is red. Charlie is blue. Charlie is quiet. Charlie is young. Fiona is blue. Fiona is smart. Gary is not big. Gary is nice. Gary is quiet. Gary is red. Gary is smart. Red, quiet people are young. If Fiona is blue and Fiona is young then Fiona is big. Smart people are quiet. Quiet people are red. If someone is nice and blue then they are not smart. If someone is quiet then they are smart. All big, quiet people are not nice. If Charlie is not big then Charlie is quiet. If Fiona is smart and Fiona is young then Fiona is quiet.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is not nice.
("Anne" "is" "nice" "-")
Anne is red.
("Anne" "is" "red" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Gary is not big.
("Gary" "is" "big" "-")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Red, quiet people are young.
((("someone" "is" "red" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
If Fiona is blue and Fiona is young then Fiona is big.
((("Fiona" "is" "blue" "+") ("Fiona" "is" "young" "+")) -> ("Fiona" "is" "big" "+"))
Smart people are quiet.
((("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
Quiet people are red.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
If someone is nice and blue then they are not smart.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "-"))
If someone is quiet then they are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
All big, quiet people are not nice.
((("someone" "is" "big" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "-"))
If Charlie is not big then Charlie is quiet.
((("Charlie" "is" "big" "~")) -> ("Charlie" "is" "quiet" "+"))
If Fiona is smart and Fiona is young then Fiona is quiet.
((("Fiona" "is" "smart" "+") ("Fiona" "is" "young" "+")) -> ("Fiona" "is" "quiet" "+"))
Charlie is young.
True
1
proof
[(triple7 OR ((((triple6) -> rule4) triple6) -> rule1))]
("Charlie" "is" "young" "+")
triple7
((((triple6) -> (rule4 % int2)) triple6) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Fiona is not blue.
False
1
inv-proof
[(triple8)]
("Fiona" "is" "blue" "-")
triple8
Charlie is smart.
True
2
proof
[(((triple6) -> rule6))]
("Charlie" "is" "smart" "+")
((triple6) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Gary is not young.
False
3
inv-proof
[(((triple13 triple12) -> rule1) OR ((triple13 ((triple14) -> rule3)) -> rule1) OR ((((triple12) -> rule4) triple12) -> rule1) OR ((((triple12) -> rule4) ((triple14) -> rule3)) -> rule1) OR ((((((triple14) -> rule3)) -> rule4) triple12) -> rule1) OR ((((((triple14) -> rule3)) -> rule4) ((triple14) -> rule3)) -> rule1))]
("Gary" "is" "young" "-")
((triple13 triple12) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((triple13 ((triple14) -> (rule3 % int2))) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((((triple12) -> (rule4 % int2)) triple12) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((triple12) -> (rule4 % int3)) ((triple14) -> (rule3 % int2))) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
((((((triple14) -> (rule3 % int3))) -> (rule4 % int2)) triple12) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((((triple14) -> (rule3 % int3))) -> (rule4 % int2)) ((triple14) -> (rule3 % int3))) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Fiona is red.
True
3
proof
[(((((triple9) -> rule3)) -> rule4))]
("Fiona" "is" "red" "+")
((((triple9) -> (rule3 % int2))) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is not red.
False
3
inv-proof
[(((((triple9) -> rule3)) -> rule4))]
("Fiona" "is" "red" "-")
((((triple9) -> (rule3 % int2))) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is young.
True
6
proof
[(((((((triple9) -> rule3)) -> rule4) ((triple9) -> rule3)) -> rule1))]
("Fiona" "is" "young" "+")
((((((triple9) -> (rule3 % int3))) -> (rule4 % int2)) ((triple9) -> (rule3 % int3))) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is not young.
False
6
inv-proof
[(((((((triple9) -> rule3)) -> rule4) ((triple9) -> rule3)) -> rule1))]
("Fiona" "is" "young" "-")
((((((triple9) -> (rule3 % int3))) -> (rule4 % int2)) ((triple9) -> (rule3 % int3))) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is big.
True
8
proof
[(((triple8 ((((((triple9) -> rule3)) -> rule4) ((triple9) -> rule3)) -> rule1)) -> rule2))]
("Fiona" "is" "big" "+")
((triple8 ((((((triple9) -> (rule3 % int4))) -> (rule4 % int3)) ((triple9) -> (rule3 % int4))) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int4
Fiona is not big.
False
8
inv-proof
[(((triple8 ((((((triple9) -> rule3)) -> rule4) ((triple9) -> rule3)) -> rule1)) -> rule2))]
("Fiona" "is" "big" "-")
((triple8 ((((((triple9) -> (rule3 % int4))) -> (rule4 % int3)) ((triple9) -> (rule3 % int4))) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int4
Fiona is not nice.
True
11
proof
[(((((triple8 ((((((triple9) -> rule3)) -> rule4) ((triple9) -> rule3)) -> rule1)) -> rule2) ((triple9) -> rule3)) -> rule7))]
("Fiona" "is" "nice" "-")
((((triple8 ((((((triple9) -> (rule3 % int5))) -> (rule4 % int4)) ((triple9) -> (rule3 % int5))) -> (rule1 % int3))) -> (rule2 % int2)) ((triple9) -> (rule3 % int5))) -> (rule7 % int1))
Fiona is not nice.
("Fiona" "is" "nice" "-")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int5
Fiona is nice.
False
11
inv-proof
[(((((triple8 ((((((triple9) -> rule3)) -> rule4) ((triple9) -> rule3)) -> rule1)) -> rule2) ((triple9) -> rule3)) -> rule7))]
("Fiona" "is" "nice" "+")
((((triple8 ((((((triple9) -> (rule3 % int5))) -> (rule4 % int4)) ((triple9) -> (rule3 % int5))) -> (rule1 % int3))) -> (rule2 % int2)) ((triple9) -> (rule3 % int5))) -> (rule7 % int1))
Fiona is not nice.
("Fiona" "is" "nice" "-")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int5
Anne is not quiet.
Unknown
inv-rconc
[@2: Anne is quiet.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("Anne" "is" "quiet" "-")
Anne is young.
Unknown
rconc
[@3: Anne is young.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule6 <- FAIL)]]
("Anne" "is" "young" "+")
Anne is not smart.
Unknown
inv-rconc
[@2: Anne is smart.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Anne" "is" "smart" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Anne is big.[(triple1)] Anne is blue.[(triple2)] Anne is not nice.[(triple3)] Anne is red.[(triple4)] Charlie is blue.[(triple5)] Charlie is quiet.[(triple6)] Charlie is young.[(triple7 OR ((((triple6) -> rule4) triple6) -> rule1))] Fiona is blue.[(triple8)] Fiona is smart.[(triple9)] Gary is nice.[(triple11)] Gary is not big.[(triple10)] Gary is quiet.[(triple12 OR ((triple14) -> rule3))] Gary is red.[(triple13 OR ((triple12) -> rule4) OR ((((triple14) -> rule3)) -> rule4))] Gary is smart.[(triple14 OR ((triple12) -> rule6))] @1: Charlie is red.[(((triple6) -> rule4))] Charlie is smart.[(((triple6) -> rule6))] Fiona is quiet.[(((triple9) -> rule3))] Gary is young.[(((triple13 triple12) -> rule1) OR ((triple13 ((triple14) -> rule3)) -> rule1) OR ((((triple12) -> rule4) triple12) -> rule1) OR ((((triple12) -> rule4) ((triple14) -> rule3)) -> rule1) OR ((((((triple14) -> rule3)) -> rule4) triple12) -> rule1) OR ((((((triple14) -> rule3)) -> rule4) ((triple14) -> rule3)) -> rule1))] @2: Fiona is red.[(((((triple9) -> rule3)) -> rule4))] @3: Fiona is young.[(((((((triple9) -> rule3)) -> rule4) ((triple9) -> rule3)) -> rule1))] @4: Fiona is big.[(((triple8 ((((((triple9) -> rule3)) -> rule4) ((triple9) -> rule3)) -> rule1)) -> rule2))] @5: Fiona is not nice.[(((((triple8 ((((((triple9) -> rule3)) -> rule4) ((triple9) -> rule3)) -> rule1)) -> rule2) ((triple9) -> rule3)) -> rule7))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is not nice.
("Anne" "is" "nice" "-")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple4
Charlie is blue.
("Charlie" "is" "blue" "+")
triple5
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple6
Charlie is young.
("Charlie" "is" "young" "+")
triple7
((((triple6) -> (rule4 % int2)) triple6) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
triple8
Fiona is smart.
("Fiona" "is" "smart" "+")
triple9
Gary is nice.
("Gary" "is" "nice" "+")
triple11
Gary is not big.
("Gary" "is" "big" "-")
triple10
Gary is quiet.
("Gary" "is" "quiet" "+")
triple12
((triple14) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
triple13
((triple12) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((triple14) -> (rule3 % int2))) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
triple14
((triple12) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((triple6) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple6) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple9) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple13 triple12) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((triple13 ((triple14) -> (rule3 % int2))) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((((triple12) -> (rule4 % int2)) triple12) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((triple12) -> (rule4 % int3)) ((triple14) -> (rule3 % int2))) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
((((((triple14) -> (rule3 % int3))) -> (rule4 % int2)) triple12) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((((triple14) -> (rule3 % int3))) -> (rule4 % int2)) ((triple14) -> (rule3 % int3))) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
((((triple9) -> (rule3 % int2))) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
((((((triple9) -> (rule3 % int3))) -> (rule4 % int2)) ((triple9) -> (rule3 % int3))) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
((triple8 ((((((triple9) -> (rule3 % int4))) -> (rule4 % int3)) ((triple9) -> (rule3 % int4))) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int4
Fiona is not nice.
("Fiona" "is" "nice" "-")
((((triple8 ((((((triple9) -> (rule3 % int5))) -> (rule4 % int4)) ((triple9) -> (rule3 % int5))) -> (rule1 % int3))) -> (rule2 % int2)) ((triple9) -> (rule3 % int5))) -> (rule7 % int1))
Fiona is not nice.
("Fiona" "is" "nice" "-")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int5