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