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