Charlie is blue. Dave is blue. Dave is red. Dave is young. Fiona is big. Fiona is red. Gary is green. Blue people are round. All green people are blue. White people are big. If someone is green and white then they are big. If someone is round then they are white. If Dave is big then Dave is red. If Fiona is green and Fiona is blue then Fiona is young. Green, big people are not red. If Charlie is green and Charlie is not white then Charlie is big.
Charlie is blue.
("Charlie" "is" "blue" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Gary is green.
("Gary" "is" "green" "+")
Blue people are round.
((("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
All green people are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
White people are big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
If someone is green and white then they are big.
((("someone" "is" "green" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
If someone is round then they are white.
((("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
If Dave is big then Dave is red.
((("Dave" "is" "big" "+")) -> ("Dave" "is" "red" "+"))
If Fiona is green and Fiona is blue then Fiona is young.
((("Fiona" "is" "green" "+") ("Fiona" "is" "blue" "+")) -> ("Fiona" "is" "young" "+"))
Green, big people are not red.
((("someone" "is" "green" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "red" "-"))
If Charlie is green and Charlie is not white then Charlie is big.
((("Charlie" "is" "green" "+") ("Charlie" "is" "white" "~")) -> ("Charlie" "is" "big" "+"))
Dave is blue.
True
1
proof
[(triple2)]
("Dave" "is" "blue" "+")
triple2
Fiona is not big.
False
1
inv-proof
[(triple5)]
("Fiona" "is" "big" "-")
triple5
Dave is round.
True
2
proof
[(((triple2) -> rule1))]
("Dave" "is" "round" "+")
((triple2) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Charlie is not round.
False
2
inv-proof
[(((triple1) -> rule1))]
("Charlie" "is" "round" "-")
((triple1) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is white.
True
3
proof
[(((((triple1) -> rule1)) -> rule5))]
("Charlie" "is" "white" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is not white.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule5))]
("Charlie" "is" "white" "-")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is big.
True
4
proof
[(((((((triple1) -> rule1)) -> rule5)) -> rule3))]
("Charlie" "is" "big" "+")
((((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is not big.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule5)) -> rule3))]
("Charlie" "is" "big" "-")
((((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Gary is big.
True
5
proof
[(((((((((triple7) -> rule2)) -> rule1)) -> rule5)) -> rule3) OR ((triple7 ((((((triple7) -> rule2)) -> rule1)) -> rule5)) -> rule4))]
("Gary" "is" "big" "+")
((((((((triple7) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
((triple7 ((((((triple7) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
Gary is not big.
False
5
inv-proof
[(((((((((triple7) -> rule2)) -> rule1)) -> rule5)) -> rule3) OR ((triple7 ((((((triple7) -> rule2)) -> rule1)) -> rule5)) -> rule4))]
("Gary" "is" "big" "-")
((((((((triple7) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
((triple7 ((((((triple7) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
Gary is not red.
True
7
proof
[(((triple7 ((((((((triple7) -> rule2)) -> rule1)) -> rule5)) -> rule3)) -> rule8) OR ((triple7 ((triple7 ((((((triple7) -> rule2)) -> rule1)) -> rule5)) -> rule4)) -> rule8))]
("Gary" "is" "red" "-")
((triple7 ((((((((triple7) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Gary is not red.
("Gary" "is" "red" "-")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
Gary is blue.
("Gary" "is" "blue" "+")
int5
((triple7 ((triple7 ((((((triple7) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Gary is not red.
("Gary" "is" "red" "-")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
Gary is blue.
("Gary" "is" "blue" "+")
int5
Gary is red.
False
7
inv-proof
[(((triple7 ((((((((triple7) -> rule2)) -> rule1)) -> rule5)) -> rule3)) -> rule8) OR ((triple7 ((triple7 ((((((triple7) -> rule2)) -> rule1)) -> rule5)) -> rule4)) -> rule8))]
("Gary" "is" "red" "+")
((triple7 ((((((((triple7) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Gary is not red.
("Gary" "is" "red" "-")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
Gary is blue.
("Gary" "is" "blue" "+")
int5
((triple7 ((triple7 ((((((triple7) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Gary is not red.
("Gary" "is" "red" "-")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
Gary is blue.
("Gary" "is" "blue" "+")
int5
Fiona is not young.
Unknown
inv-rconc
[@1: Fiona is young.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Fiona" "is" "young" "-")
Fiona is blue.
Unknown
rconc
[@1: Fiona is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "blue" "+")
Fiona is not white.
Unknown
inv-rconc
[@3: Fiona is white.[CWA. Example of deepest failure = (rule5 <- rule1 <- rule2 <- FAIL)]]
("Fiona" "is" "white" "-")
Fiona is round.
Unknown
rconc
[@2: Fiona is round.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Fiona" "is" "round" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
Fiona is not green.
Unknown
inv-random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
@0: Charlie is blue.[(triple1)] Dave is blue.[(triple2)] Dave is red.[(triple3 OR ((((((((triple2) -> rule1)) -> rule5)) -> rule3)) -> rule6))] Dave is young.[(triple4)] Fiona is big.[(triple5)] Fiona is red.[(triple6)] Gary is green.[(triple7)] @1: Charlie is round.[(((triple1) -> rule1))] Dave is round.[(((triple2) -> rule1))] Gary is blue.[(((triple7) -> rule2))] @2: Charlie is white.[(((((triple1) -> rule1)) -> rule5))] Dave is white.[(((((triple2) -> rule1)) -> rule5))] Gary is round.[(((((triple7) -> rule2)) -> rule1))] @3: Charlie is big.[(((((((triple1) -> rule1)) -> rule5)) -> rule3))] Dave is big.[(((((((triple2) -> rule1)) -> rule5)) -> rule3))] Gary is white.[(((((((triple7) -> rule2)) -> rule1)) -> rule5))] @4: Gary is big.[(((((((((triple7) -> rule2)) -> rule1)) -> rule5)) -> rule3) OR ((triple7 ((((((triple7) -> rule2)) -> rule1)) -> rule5)) -> rule4))] @5: Gary is not red.[(((triple7 ((((((((triple7) -> rule2)) -> rule1)) -> rule5)) -> rule3)) -> rule8) OR ((triple7 ((triple7 ((((((triple7) -> rule2)) -> rule1)) -> rule5)) -> rule4)) -> rule8))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Dave is red.
("Dave" "is" "red" "+")
triple3
((((((((triple2) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is young.
("Dave" "is" "young" "+")
triple4
Fiona is big.
("Fiona" "is" "big" "+")
triple5
Fiona is red.
("Fiona" "is" "red" "+")
triple6
Gary is green.
("Gary" "is" "green" "+")
triple7
Charlie is round.
("Charlie" "is" "round" "+")
((triple1) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple2) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple7) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
((((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
((((((triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
((((((triple7) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
((((((((triple7) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
((triple7 ((((((triple7) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
Gary is not red.
("Gary" "is" "red" "-")
((triple7 ((((((((triple7) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Gary is not red.
("Gary" "is" "red" "-")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
Gary is blue.
("Gary" "is" "blue" "+")
int5
((triple7 ((triple7 ((((((triple7) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Gary is not red.
("Gary" "is" "red" "-")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
Gary is blue.
("Gary" "is" "blue" "+")
int5