Anne is white. Anne is young. Fiona is big. Fiona is blue. Fiona is cold. Fiona is green. Fiona is white. Fiona is young. Gary is not big. Gary is cold. Gary is smart. Gary is young. Smart people are blue. If someone is blue then they are white. If Fiona is big then Fiona is white. If Fiona is young and Fiona is green then Fiona is smart. All white people are green. All cold, smart people are young.
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is not big.
("Gary" "is" "big" "-")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
Smart people are blue.
((("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
If someone is blue then they are white.
((("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
If Fiona is big then Fiona is white.
((("Fiona" "is" "big" "+")) -> ("Fiona" "is" "white" "+"))
If Fiona is young and Fiona is green then Fiona is smart.
((("Fiona" "is" "young" "+") ("Fiona" "is" "green" "+")) -> ("Fiona" "is" "smart" "+"))
All white people are green.
((("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
All cold, smart people are young.
((("someone" "is" "cold" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
Fiona is white.
True
1
proof
[(triple7 OR ((triple3) -> rule3) OR ((triple4) -> rule2) OR ((((((triple8 triple6) -> rule4)) -> rule1)) -> rule2))]
("Fiona" "is" "white" "+")
triple7
((triple3) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((triple4) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((((((triple8 triple6) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is not cold.
False
1
inv-proof
[(triple5)]
("Fiona" "is" "cold" "-")
triple5
Fiona is smart.
True
3
proof
[(((triple8 triple6) -> rule4) OR ((triple8 ((triple7) -> rule5)) -> rule4) OR ((triple8 ((((triple3) -> rule3)) -> rule5)) -> rule4) OR ((triple8 ((((triple4) -> rule2)) -> rule5)) -> rule4))]
("Fiona" "is" "smart" "+")
((triple8 triple6) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((triple8 ((triple7) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
((triple8 ((((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
((triple8 ((((triple4) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is not smart.
False
3
inv-proof
[(((triple8 triple6) -> rule4) OR ((triple8 ((triple7) -> rule5)) -> rule4) OR ((triple8 ((((triple3) -> rule3)) -> rule5)) -> rule4) OR ((triple8 ((((triple4) -> rule2)) -> rule5)) -> rule4))]
("Fiona" "is" "smart" "-")
((triple8 triple6) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((triple8 ((triple7) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
((triple8 ((((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
((triple8 ((((triple4) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Gary is white.
True
3
proof
[(((((triple11) -> rule1)) -> rule2))]
("Gary" "is" "white" "+")
((((triple11) -> (rule1 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is not white.
False
3
inv-proof
[(((((triple11) -> rule1)) -> rule2))]
("Gary" "is" "white" "-")
((((triple11) -> (rule1 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is green.
True
4
proof
[(((((((triple11) -> rule1)) -> rule2)) -> rule5))]
("Gary" "is" "green" "+")
((((((triple11) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is not green.
False
4
inv-proof
[(((((((triple11) -> rule1)) -> rule2)) -> rule5))]
("Gary" "is" "green" "-")
((((((triple11) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Anne is not blue.
Unknown
inv-rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "blue" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
Anne is not cold.
Unknown
inv-random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is white.[(triple1)] Anne is young.[(triple2)] Fiona is big.[(triple3)] Fiona is blue.[(triple4 OR ((((triple8 triple6) -> rule4)) -> rule1) OR ((((triple8 ((triple7) -> rule5)) -> rule4)) -> rule1) OR ((((triple8 ((((triple3) -> rule3)) -> rule5)) -> rule4)) -> rule1))] Fiona is cold.[(triple5)] Fiona is green.[(triple6 OR ((triple7) -> rule5) OR ((((triple3) -> rule3)) -> rule5) OR ((((triple4) -> rule2)) -> rule5))] Fiona is white.[(triple7 OR ((triple3) -> rule3) OR ((triple4) -> rule2) OR ((((((triple8 triple6) -> rule4)) -> rule1)) -> rule2))] Fiona is young.[(triple8)] Gary is cold.[(triple10)] Gary is not big.[(triple9)] Gary is smart.[(triple11)] Gary is young.[(triple12 OR ((triple10 triple11) -> rule6))] @1: Anne is green.[(((triple1) -> rule5))] Fiona is smart.[(((triple8 triple6) -> rule4) OR ((triple8 ((triple7) -> rule5)) -> rule4) OR ((triple8 ((((triple3) -> rule3)) -> rule5)) -> rule4) OR ((triple8 ((((triple4) -> rule2)) -> rule5)) -> rule4))] Gary is blue.[(((triple11) -> rule1))] @2: Gary is white.[(((((triple11) -> rule1)) -> rule2))] @3: Gary is green.[(((((((triple11) -> rule1)) -> rule2)) -> rule5))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Anne is young.
("Anne" "is" "young" "+")
triple2
Fiona is big.
("Fiona" "is" "big" "+")
triple3
Fiona is blue.
("Fiona" "is" "blue" "+")
triple4
((((triple8 triple6) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((triple8 ((triple7) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
((((triple8 ((((triple3) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
int4
Fiona is cold.
("Fiona" "is" "cold" "+")
triple5
Fiona is green.
("Fiona" "is" "green" "+")
triple6
((triple7) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
((((triple4) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
triple7
((triple3) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((triple4) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((((((triple8 triple6) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is young.
("Fiona" "is" "young" "+")
triple8
Gary is cold.
("Gary" "is" "cold" "+")
triple10
Gary is not big.
("Gary" "is" "big" "-")
triple9
Gary is smart.
("Gary" "is" "smart" "+")
triple11
Gary is young.
("Gary" "is" "young" "+")
triple12
((triple10 triple11) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple8 triple6) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((triple8 ((triple7) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
((triple8 ((((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
((triple8 ((((triple4) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
((triple11) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((((triple11) -> (rule1 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
((((((triple11) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3