Anne is not green. Anne is red. Charlie is blue. Charlie is smart. Fiona is red. Harry is quiet. Harry is red. If someone is green then they are blue. If someone is smart and red then they are blue. Blue, smart people are green. Quiet people are big. All green people are not furry. Big people are smart. If Fiona is quiet and Fiona is not red then Fiona is furry.
Anne is not green.
("Anne" "is" "green" "-")
Anne is red.
("Anne" "is" "red" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
If someone is green then they are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
If someone is smart and red then they are blue.
((("someone" "is" "smart" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
Blue, smart people are green.
((("someone" "is" "blue" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
Quiet people are big.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
All green people are not furry.
((("someone" "is" "green" "+")) -> ("someone" "is" "furry" "-"))
Big people are smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
If Fiona is quiet and Fiona is not red then Fiona is furry.
((("Fiona" "is" "quiet" "+") ("Fiona" "is" "red" "~")) -> ("Fiona" "is" "furry" "+"))
Fiona is red.
True
1
proof
[(triple5)]
("Fiona" "is" "red" "+")
triple5
Anne is not red.
False
1
inv-proof
[(triple2)]
("Anne" "is" "red" "-")
triple2
Charlie is green.
True
3
proof
[(((triple3 triple4) -> rule3))]
("Charlie" "is" "green" "+")
((triple3 triple4) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Harry is not big.
False
2
inv-proof
[(((triple6) -> rule4))]
("Harry" "is" "big" "-")
((triple6) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Charlie is not furry.
True
4
proof
[(((((triple3 triple4) -> rule3)) -> rule5))]
("Charlie" "is" "furry" "-")
((((triple3 triple4) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Harry is not smart.
False
3
inv-proof
[(((((triple6) -> rule4)) -> rule6))]
("Harry" "is" "smart" "-")
((((triple6) -> (rule4 % int2))) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is blue.
True
5
proof
[(((((((triple6) -> rule4)) -> rule6) triple7) -> rule2))]
("Harry" "is" "blue" "+")
((((((triple6) -> (rule4 % int3))) -> (rule6 % int2)) triple7) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is not blue.
False
5
inv-proof
[(((((((triple6) -> rule4)) -> rule6) triple7) -> rule2))]
("Harry" "is" "blue" "-")
((((((triple6) -> (rule4 % int3))) -> (rule6 % int2)) triple7) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is green.
True
9
proof
[(((((((((triple6) -> rule4)) -> rule6) triple7) -> rule2) ((((triple6) -> rule4)) -> rule6)) -> rule3))]
("Harry" "is" "green" "+")
((((((((triple6) -> (rule4 % int4))) -> (rule6 % int3)) triple7) -> (rule2 % int2)) ((((triple6) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
Harry is not green.
False
9
inv-proof
[(((((((((triple6) -> rule4)) -> rule6) triple7) -> rule2) ((((triple6) -> rule4)) -> rule6)) -> rule3))]
("Harry" "is" "green" "-")
((((((((triple6) -> (rule4 % int4))) -> (rule6 % int3)) triple7) -> (rule2 % int2)) ((((triple6) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
Harry is not furry.
True
10
proof
[(((((((((((triple6) -> rule4)) -> rule6) triple7) -> rule2) ((((triple6) -> rule4)) -> rule6)) -> rule3)) -> rule5))]
("Harry" "is" "furry" "-")
((((((((((triple6) -> (rule4 % int5))) -> (rule6 % int4)) triple7) -> (rule2 % int3)) ((((triple6) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule3 % int2))) -> (rule5 % int1))
Harry is not furry.
("Harry" "is" "furry" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
Harry is big.
("Harry" "is" "big" "+")
int5
Harry is furry.
False
10
inv-proof
[(((((((((((triple6) -> rule4)) -> rule6) triple7) -> rule2) ((((triple6) -> rule4)) -> rule6)) -> rule3)) -> rule5))]
("Harry" "is" "furry" "+")
((((((((((triple6) -> (rule4 % int5))) -> (rule6 % int4)) triple7) -> (rule2 % int3)) ((((triple6) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule3 % int2))) -> (rule5 % int1))
Harry is not furry.
("Harry" "is" "furry" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
Harry is big.
("Harry" "is" "big" "+")
int5
Fiona is not blue.
Unknown
inv-rconc
[@4: Fiona is blue.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule6 <- rule4 <- FAIL)]]
("Fiona" "is" "blue" "-")
Fiona is smart.
Unknown
rconc
[@2: Fiona is smart.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Fiona" "is" "smart" "+")
Anne is not blue.
Unknown
inv-rconc
[@3: Anne is blue.[CWA. Example of deepest failure = (rule2 <- rule6 <- rule4 <- FAIL)]]
("Anne" "is" "blue" "-")
Anne is smart.
Unknown
rconc
[@2: Anne is smart.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Anne" "is" "smart" "+")
Anne is not big.
Unknown
inv-rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "big" "-")
Fiona is green.
Unknown
rconc
[@3: Fiona is green.[CWA. Example of deepest failure = (rule3 <- rule6 <- rule4 <- FAIL)]]
("Fiona" "is" "green" "+")
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
@0: Anne is not green.[(triple1)] Anne is red.[(triple2)] Charlie is blue.[(triple3)] Charlie is smart.[(triple4)] Fiona is red.[(triple5)] Harry is quiet.[(triple6)] Harry is red.[(triple7)] @1: Charlie is green.[(((triple3 triple4) -> rule3))] Harry is big.[(((triple6) -> rule4))] @2: Charlie is not furry.[(((((triple3 triple4) -> rule3)) -> rule5))] Harry is smart.[(((((triple6) -> rule4)) -> rule6))] @3: Harry is blue.[(((((((triple6) -> rule4)) -> rule6) triple7) -> rule2))] @4: Harry is green.[(((((((((triple6) -> rule4)) -> rule6) triple7) -> rule2) ((((triple6) -> rule4)) -> rule6)) -> rule3))] @5: Harry is not furry.[(((((((((((triple6) -> rule4)) -> rule6) triple7) -> rule2) ((((triple6) -> rule4)) -> rule6)) -> rule3)) -> rule5))]
Anne is not green.
("Anne" "is" "green" "-")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple3
Charlie is smart.
("Charlie" "is" "smart" "+")
triple4
Fiona is red.
("Fiona" "is" "red" "+")
triple5
Harry is quiet.
("Harry" "is" "quiet" "+")
triple6
Harry is red.
("Harry" "is" "red" "+")
triple7
Charlie is green.
("Charlie" "is" "green" "+")
((triple3 triple4) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple6) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Charlie is not furry.
("Charlie" "is" "furry" "-")
((((triple3 triple4) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((((triple6) -> (rule4 % int2))) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
((((((triple6) -> (rule4 % int3))) -> (rule6 % int2)) triple7) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
((((((((triple6) -> (rule4 % int4))) -> (rule6 % int3)) triple7) -> (rule2 % int2)) ((((triple6) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
Harry is not furry.
("Harry" "is" "furry" "-")
((((((((((triple6) -> (rule4 % int5))) -> (rule6 % int4)) triple7) -> (rule2 % int3)) ((((triple6) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule3 % int2))) -> (rule5 % int1))
Harry is not furry.
("Harry" "is" "furry" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
Harry is big.
("Harry" "is" "big" "+")
int5