Anne is big. Anne is furry. Anne is nice. Anne is red. Anne is white. Bob is big. Bob is furry. Bob is red. Charlie is big. Charlie is round. Fiona is nice. Fiona is red. All big, round people are red. All quiet people are furry. If Charlie is red then Charlie is quiet. All quiet, white people are furry. If someone is quiet then they are furry. Furry people are round.
Anne is big.
("Anne" "is" "big" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is red.
("Bob" "is" "red" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is red.
("Fiona" "is" "red" "+")
All big, round people are red.
((("someone" "is" "big" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
All quiet people are furry.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "+"))
If Charlie is red then Charlie is quiet.
((("Charlie" "is" "red" "+")) -> ("Charlie" "is" "quiet" "+"))
All quiet, white people are furry.
((("someone" "is" "quiet" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
If someone is quiet then they are furry.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "+"))
Furry people are round.
((("someone" "is" "furry" "+")) -> ("someone" "is" "round" "+"))
Charlie is round.
True
1
proof
[(triple10)]
("Charlie" "is" "round" "+")
triple10
Bob is not red.
False
1
inv-proof
[(triple8 OR ((triple6 ((triple7) -> rule6)) -> rule1))]
("Bob" "is" "red" "-")
triple8
((triple6 ((triple7) -> (rule6 % int2))) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is round.
True
2
proof
[(((triple7) -> rule6))]
("Bob" "is" "round" "+")
((triple7) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Charlie is not red.
False
3
inv-proof
[(((triple9 triple10) -> rule1))]
("Charlie" "is" "red" "-")
((triple9 triple10) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is quiet.
True
4
proof
[(((((triple9 triple10) -> rule1)) -> rule3))]
("Charlie" "is" "quiet" "+")
((((triple9 triple10) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is not quiet.
False
4
inv-proof
[(((((triple9 triple10) -> rule1)) -> rule3))]
("Charlie" "is" "quiet" "-")
((((triple9 triple10) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is furry.
True
5
proof
[(((((((triple9 triple10) -> rule1)) -> rule3)) -> rule2) OR ((((((triple9 triple10) -> rule1)) -> rule3)) -> rule5))]
("Charlie" "is" "furry" "+")
((((((triple9 triple10) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
((((((triple9 triple10) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is not furry.
False
5
inv-proof
[(((((((triple9 triple10) -> rule1)) -> rule3)) -> rule2) OR ((((((triple9 triple10) -> rule1)) -> rule3)) -> rule5))]
("Charlie" "is" "furry" "-")
((((((triple9 triple10) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
((((((triple9 triple10) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Fiona is not round.
Unknown
inv-rconc
[@2: Fiona is round.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("Fiona" "is" "round" "-")
Fiona is furry.
Unknown
rconc
[@1: Fiona is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "furry" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
Fiona is not big.
Unknown
inv-random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
@0: Anne is big.[(triple1)] Anne is furry.[(triple2)] Anne is nice.[(triple3)] Anne is red.[(triple4 OR ((triple1 ((triple2) -> rule6)) -> rule1))] Anne is white.[(triple5)] Bob is big.[(triple6)] Bob is furry.[(triple7)] Bob is red.[(triple8 OR ((triple6 ((triple7) -> rule6)) -> rule1))] Charlie is big.[(triple9)] Charlie is round.[(triple10)] Fiona is nice.[(triple11)] Fiona is red.[(triple12)] @1: Anne is round.[(((triple2) -> rule6))] Bob is round.[(((triple7) -> rule6))] Charlie is red.[(((triple9 triple10) -> rule1))] @2: Charlie is quiet.[(((((triple9 triple10) -> rule1)) -> rule3))] @3: Charlie is furry.[(((((((triple9 triple10) -> rule1)) -> rule3)) -> rule2) OR ((((((triple9 triple10) -> rule1)) -> rule3)) -> rule5))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple4
((triple1 ((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
triple5
Bob is big.
("Bob" "is" "big" "+")
triple6
Bob is furry.
("Bob" "is" "furry" "+")
triple7
Bob is red.
("Bob" "is" "red" "+")
triple8
((triple6 ((triple7) -> (rule6 % int2))) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
triple9
Charlie is round.
("Charlie" "is" "round" "+")
triple10
Fiona is nice.
("Fiona" "is" "nice" "+")
triple11
Fiona is red.
("Fiona" "is" "red" "+")
triple12
Anne is round.
("Anne" "is" "round" "+")
((triple2) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((triple7) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((triple9 triple10) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple9 triple10) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
((((((triple9 triple10) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
((((((triple9 triple10) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3