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