Anne is round. Erin is nice. Erin is white. Fiona is big. Fiona is red. Harry is nice. Harry is white. If Anne is blue and Anne is nice then Anne is red. If someone is blue then they are white. White people are big. If someone is blue and quiet then they are round. Nice, big people are quiet. If someone is white and quiet then they are big. If someone is round then they are blue. If someone is big and round then they are nice. All quiet people are nice.
Anne is round.
("Anne" "is" "round" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is white.
("Harry" "is" "white" "+")
If Anne is blue and Anne is nice then Anne is red.
((("Anne" "is" "blue" "+") ("Anne" "is" "nice" "+")) -> ("Anne" "is" "red" "+"))
If someone is blue then they are white.
((("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
White people are big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
If someone is blue and quiet then they are round.
((("someone" "is" "blue" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
Nice, big people are quiet.
((("someone" "is" "nice" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
If someone is white and quiet then they are big.
((("someone" "is" "white" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
If someone is round then they are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
If someone is big and round then they are nice.
((("someone" "is" "big" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
All quiet people are nice.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
Fiona is big.
True
1
proof
[(triple4)]
("Fiona" "is" "big" "+")
triple4
Fiona is not big.
False
1
inv-proof
[(triple4)]
("Fiona" "is" "big" "-")
triple4
Erin is big.
True
2
proof
[(((triple3) -> rule3))]
("Erin" "is" "big" "+")
((triple3) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is not big.
False
2
inv-proof
[(((triple3) -> rule3))]
("Erin" "is" "big" "-")
((triple3) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is quiet.
True
4
proof
[(((triple2 ((triple3) -> rule3)) -> rule5))]
("Erin" "is" "quiet" "+")
((triple2 ((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is not quiet.
False
4
inv-proof
[(((triple2 ((triple3) -> rule3)) -> rule5))]
("Erin" "is" "quiet" "-")
((triple2 ((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Anne is big.
True
4
proof
[(((((((triple1) -> rule7)) -> rule2)) -> rule3))]
("Anne" "is" "big" "+")
((((((triple1) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is not big.
False
4
inv-proof
[(((((((triple1) -> rule7)) -> rule2)) -> rule3))]
("Anne" "is" "big" "-")
((((((triple1) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is nice.
True
6
proof
[(((((((((triple1) -> rule7)) -> rule2)) -> rule3) triple1) -> rule8))]
("Anne" "is" "nice" "+")
((((((((triple1) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule3 % int2)) triple1) -> (rule8 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
int4
Anne is not nice.
False
6
inv-proof
[(((((((((triple1) -> rule7)) -> rule2)) -> rule3) triple1) -> rule8))]
("Anne" "is" "nice" "-")
((((((((triple1) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule3 % int2)) triple1) -> (rule8 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
int4
Anne is quiet.
True
11
proof
[(((((((((((triple1) -> rule7)) -> rule2)) -> rule3) triple1) -> rule8) ((((((triple1) -> rule7)) -> rule2)) -> rule3)) -> rule5))]
("Anne" "is" "quiet" "+")
((((((((((triple1) -> (rule7 % int5))) -> (rule2 % int4))) -> (rule3 % int3)) triple1) -> (rule8 % int2)) ((((((triple1) -> (rule7 % int5))) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
Anne is blue.
("Anne" "is" "blue" "+")
int5
Anne is not quiet.
False
11
inv-proof
[(((((((((((triple1) -> rule7)) -> rule2)) -> rule3) triple1) -> rule8) ((((((triple1) -> rule7)) -> rule2)) -> rule3)) -> rule5))]
("Anne" "is" "quiet" "-")
((((((((((triple1) -> (rule7 % int5))) -> (rule2 % int4))) -> (rule3 % int3)) triple1) -> (rule8 % int2)) ((((((triple1) -> (rule7 % int5))) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
Anne is blue.
("Anne" "is" "blue" "+")
int5
Harry is not round.
Unknown
inv-rconc
[@2: Harry is round.[CWA. Example of deepest failure = (rule4 <- rule7 <- FAIL)]]
("Harry" "is" "round" "-")
Fiona is white.
Unknown
rconc
[@3: Fiona is white.[CWA. Example of deepest failure = (rule2 <- rule7 <- rule4 <- FAIL)]]
("Fiona" "is" "white" "+")
Fiona is not quiet.
Unknown
inv-rconc
[@3: Fiona is quiet.[CWA. Example of deepest failure = (rule5 <- rule8 <- rule4 <- FAIL)]]
("Fiona" "is" "quiet" "-")
Harry is blue.
Unknown
rconc
[@2: Harry is blue.[CWA. Example of deepest failure = (rule7 <- rule4 <- FAIL)]]
("Harry" "is" "blue" "+")
Erin is not blue.
Unknown
inv-rconc
[@2: Erin is blue.[CWA. Example of deepest failure = (rule7 <- rule4 <- FAIL)]]
("Erin" "is" "blue" "-")
Fiona is nice.
Unknown
rconc
[@4: Fiona is nice.[CWA. Example of deepest failure = (rule9 <- rule5 <- rule8 <- rule4 <- FAIL)]]
("Fiona" "is" "nice" "+")
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
@0: Anne is round.[(triple1)] Erin is nice.[(triple2)] Erin is white.[(triple3)] Fiona is big.[(triple4)] Fiona is red.[(triple5)] Harry is nice.[(triple6)] Harry is white.[(triple7)] @1: Anne is blue.[(((triple1) -> rule7))] Erin is big.[(((triple3) -> rule3))] Harry is big.[(((triple7) -> rule3))] @2: Anne is white.[(((((triple1) -> rule7)) -> rule2))] Erin is quiet.[(((triple2 ((triple3) -> rule3)) -> rule5))] Harry is quiet.[(((triple6 ((triple7) -> rule3)) -> rule5))] @3: Anne is big.[(((((((triple1) -> rule7)) -> rule2)) -> rule3))] @4: Anne is nice.[(((((((((triple1) -> rule7)) -> rule2)) -> rule3) triple1) -> rule8))] @5: Anne is quiet.[(((((((((((triple1) -> rule7)) -> rule2)) -> rule3) triple1) -> rule8) ((((((triple1) -> rule7)) -> rule2)) -> rule3)) -> rule5))] Anne is red.[(((((triple1) -> rule7) ((((((((triple1) -> rule7)) -> rule2)) -> rule3) triple1) -> rule8)) -> rule1))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Erin is nice.
("Erin" "is" "nice" "+")
triple2
Erin is white.
("Erin" "is" "white" "+")
triple3
Fiona is big.
("Fiona" "is" "big" "+")
triple4
Fiona is red.
("Fiona" "is" "red" "+")
triple5
Harry is nice.
("Harry" "is" "nice" "+")
triple6
Harry is white.
("Harry" "is" "white" "+")
triple7
Anne is blue.
("Anne" "is" "blue" "+")
((triple1) -> (rule7 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((triple3) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple7) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((((triple1) -> (rule7 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple2 ((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple6 ((triple7) -> (rule3 % int2))) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
((((((triple1) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
((((((((triple1) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule3 % int2)) triple1) -> (rule8 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
int4
Anne is quiet.
("Anne" "is" "quiet" "+")
((((((((((triple1) -> (rule7 % int5))) -> (rule2 % int4))) -> (rule3 % int3)) triple1) -> (rule8 % int2)) ((((((triple1) -> (rule7 % int5))) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
Anne is blue.
("Anne" "is" "blue" "+")
int5
Anne is red.
("Anne" "is" "red" "+")
((((triple1) -> (rule7 % int5)) ((((((((triple1) -> (rule7 % int5))) -> (rule2 % int4))) -> (rule3 % int3)) triple1) -> (rule8 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
Anne is blue.
("Anne" "is" "blue" "+")
int5