Anne is cold. Anne is smart. Bob is big. Bob is cold. Bob is nice. Bob is not rough. Bob is smart. Charlie is not cold. Charlie is nice. Charlie is rough. Charlie is smart. Gary is quiet. Rough people are nice. Rough, big people are nice. If someone is furry and quiet then they are big. If Anne is furry and Anne is smart then Anne is quiet. All big people are furry. If someone is cold and quiet then they are rough. If Anne is smart then Anne is big. If someone is rough then they are quiet.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is not rough.
("Bob" "is" "rough" "-")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is not cold.
("Charlie" "is" "cold" "-")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Rough people are nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
Rough, big people are nice.
((("someone" "is" "rough" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
If someone is furry and quiet then they are big.
((("someone" "is" "furry" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
If Anne is furry and Anne is smart then Anne is quiet.
((("Anne" "is" "furry" "+") ("Anne" "is" "smart" "+")) -> ("Anne" "is" "quiet" "+"))
All big people are furry.
((("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
If someone is cold and quiet then they are rough.
((("someone" "is" "cold" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
If Anne is smart then Anne is big.
((("Anne" "is" "smart" "+")) -> ("Anne" "is" "big" "+"))
If someone is rough then they are quiet.
((("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
Charlie is rough.
True
1
proof
[(triple10)]
("Charlie" "is" "rough" "+")
triple10
Bob is not smart.
False
1
inv-proof
[(triple7)]
("Bob" "is" "smart" "-")
triple7
Anne is big.
True
2
proof
[(((triple2) -> rule7))]
("Anne" "is" "big" "+")
((triple2) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Charlie is not quiet.
False
2
inv-proof
[(((triple10) -> rule8))]
("Charlie" "is" "quiet" "-")
((triple10) -> (rule8 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Anne is furry.
True
3
proof
[(((((triple2) -> rule7)) -> rule5))]
("Anne" "is" "furry" "+")
((((triple2) -> (rule7 % int2))) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not furry.
False
3
inv-proof
[(((((triple2) -> rule7)) -> rule5))]
("Anne" "is" "furry" "-")
((((triple2) -> (rule7 % int2))) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is quiet.
True
5
proof
[(((((((triple2) -> rule7)) -> rule5) triple2) -> rule4))]
("Anne" "is" "quiet" "+")
((((((triple2) -> (rule7 % int3))) -> (rule5 % int2)) triple2) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is not quiet.
False
5
inv-proof
[(((((((triple2) -> rule7)) -> rule5) triple2) -> rule4))]
("Anne" "is" "quiet" "-")
((((((triple2) -> (rule7 % int3))) -> (rule5 % int2)) triple2) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is rough.
True
7
proof
[(((triple1 ((((((triple2) -> rule7)) -> rule5) triple2) -> rule4)) -> rule6))]
("Anne" "is" "rough" "+")
((triple1 ((((((triple2) -> (rule7 % int4))) -> (rule5 % int3)) triple2) -> (rule4 % int2))) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Anne is not rough.
False
7
inv-proof
[(((triple1 ((((((triple2) -> rule7)) -> rule5) triple2) -> rule4)) -> rule6))]
("Anne" "is" "rough" "-")
((triple1 ((((((triple2) -> (rule7 % int4))) -> (rule5 % int3)) triple2) -> (rule4 % int2))) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Anne is nice.
True
8
proof
[(((((triple1 ((((((triple2) -> rule7)) -> rule5) triple2) -> rule4)) -> rule6)) -> rule1) OR ((((triple1 ((((((triple2) -> rule7)) -> rule5) triple2) -> rule4)) -> rule6) ((triple2) -> rule7)) -> rule2))]
("Anne" "is" "nice" "+")
((((triple1 ((((((triple2) -> (rule7 % int5))) -> (rule5 % int4)) triple2) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is big.
("Anne" "is" "big" "+")
int5
((((triple1 ((((((triple2) -> (rule7 % int5))) -> (rule5 % int4)) triple2) -> (rule4 % int3))) -> (rule6 % int2)) ((triple2) -> (rule7 % int5))) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is big.
("Anne" "is" "big" "+")
int5
Anne is not nice.
False
8
inv-proof
[(((((triple1 ((((((triple2) -> rule7)) -> rule5) triple2) -> rule4)) -> rule6)) -> rule1) OR ((((triple1 ((((((triple2) -> rule7)) -> rule5) triple2) -> rule4)) -> rule6) ((triple2) -> rule7)) -> rule2))]
("Anne" "is" "nice" "-")
((((triple1 ((((((triple2) -> (rule7 % int5))) -> (rule5 % int4)) triple2) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is big.
("Anne" "is" "big" "+")
int5
((((triple1 ((((((triple2) -> (rule7 % int5))) -> (rule5 % int4)) triple2) -> (rule4 % int3))) -> (rule6 % int2)) ((triple2) -> (rule7 % int5))) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is big.
("Anne" "is" "big" "+")
int5
Gary is not big.
Unknown
inv-rconc
[@2: Gary is big.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Gary" "is" "big" "-")
Gary is nice.
Unknown
rconc
[@2: Gary is nice.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("Gary" "is" "nice" "+")
Gary is not rough.
Unknown
inv-rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "rough" "-")
Charlie is big.
Unknown
rconc
[@2: Charlie is big.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Charlie" "is" "big" "+")
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Bob" "is" "quiet" "-")
Gary is furry.
Unknown
rconc
[@2: Gary is furry.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Gary" "is" "furry" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
@0: Anne is cold.[(triple1)] Anne is smart.[(triple2)] Bob is big.[(triple3)] Bob is cold.[(triple4)] Bob is nice.[(triple5)] Bob is not rough.[(triple6)] Bob is smart.[(triple7)] Charlie is nice.[(triple9 OR ((triple10) -> rule1))] Charlie is not cold.[(triple8)] Charlie is rough.[(triple10)] Charlie is smart.[(triple11)] Gary is quiet.[(triple12)] @1: Anne is big.[(((triple2) -> rule7))] Bob is furry.[(((triple3) -> rule5))] Charlie is quiet.[(((triple10) -> rule8))] @2: Anne is furry.[(((((triple2) -> rule7)) -> rule5))] @3: Anne is quiet.[(((((((triple2) -> rule7)) -> rule5) triple2) -> rule4))] @4: Anne is rough.[(((triple1 ((((((triple2) -> rule7)) -> rule5) triple2) -> rule4)) -> rule6))] @5: Anne is nice.[(((((triple1 ((((((triple2) -> rule7)) -> rule5) triple2) -> rule4)) -> rule6)) -> rule1) OR ((((triple1 ((((((triple2) -> rule7)) -> rule5) triple2) -> rule4)) -> rule6) ((triple2) -> rule7)) -> rule2))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
Bob is big.
("Bob" "is" "big" "+")
triple3
Bob is cold.
("Bob" "is" "cold" "+")
triple4
Bob is nice.
("Bob" "is" "nice" "+")
triple5
Bob is not rough.
("Bob" "is" "rough" "-")
triple6
Bob is smart.
("Bob" "is" "smart" "+")
triple7
Charlie is nice.
("Charlie" "is" "nice" "+")
triple9
((triple10) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple8
Charlie is rough.
("Charlie" "is" "rough" "+")
triple10
Charlie is smart.
("Charlie" "is" "smart" "+")
triple11
Gary is quiet.
("Gary" "is" "quiet" "+")
triple12
Anne is big.
("Anne" "is" "big" "+")
((triple2) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((triple3) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple10) -> (rule8 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((((triple2) -> (rule7 % int2))) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
((((((triple2) -> (rule7 % int3))) -> (rule5 % int2)) triple2) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
((triple1 ((((((triple2) -> (rule7 % int4))) -> (rule5 % int3)) triple2) -> (rule4 % int2))) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Anne is nice.
("Anne" "is" "nice" "+")
((((triple1 ((((((triple2) -> (rule7 % int5))) -> (rule5 % int4)) triple2) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is big.
("Anne" "is" "big" "+")
int5
((((triple1 ((((((triple2) -> (rule7 % int5))) -> (rule5 % int4)) triple2) -> (rule4 % int3))) -> (rule6 % int2)) ((triple2) -> (rule7 % int5))) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is big.
("Anne" "is" "big" "+")
int5