Bob is not cold. Charlie is big. Fiona is not big. All big, white people are green. Young people are green. If someone is green and young then they are furry. If Charlie is young and Charlie is not red then Charlie is not cold. All cold people are not young. If someone is big then they are young. If someone is green then they are young. If Bob is furry and Bob is not green then Bob is red.
Bob is not cold.
("Bob" "is" "cold" "-")
Charlie is big.
("Charlie" "is" "big" "+")
Fiona is not big.
("Fiona" "is" "big" "-")
All big, white people are green.
((("someone" "is" "big" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
Young people are green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
If someone is green and young then they are furry.
((("someone" "is" "green" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
If Charlie is young and Charlie is not red then Charlie is not cold.
((("Charlie" "is" "young" "+") ("Charlie" "is" "red" "~")) -> ("Charlie" "is" "cold" "-"))
All cold people are not young.
((("someone" "is" "cold" "+")) -> ("someone" "is" "young" "-"))
If someone is big then they are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
If someone is green then they are young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
If Bob is furry and Bob is not green then Bob is red.
((("Bob" "is" "furry" "+") ("Bob" "is" "green" "~")) -> ("Bob" "is" "red" "+"))
Charlie is big.
True
1
proof
[(triple2)]
("Charlie" "is" "big" "+")
triple2
Bob is cold.
False
1
inv-proof
[(triple1)]
("Bob" "is" "cold" "+")
triple1
Charlie is young.
True
2
proof
[(((triple2) -> rule6))]
("Charlie" "is" "young" "+")
((triple2) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is not young.
False
2
inv-proof
[(((triple2) -> rule6))]
("Charlie" "is" "young" "-")
((triple2) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is green.
True
3
proof
[(((((triple2) -> rule6)) -> rule2))]
("Charlie" "is" "green" "+")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is not green.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule2))]
("Charlie" "is" "green" "-")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is furry.
True
6
proof
[(((((((triple2) -> rule6)) -> rule2) ((triple2) -> rule6)) -> rule3))]
("Charlie" "is" "furry" "+")
((((((triple2) -> (rule6 % int3))) -> (rule2 % int2)) ((triple2) -> (rule6 % int3))) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is not furry.
False
6
inv-proof
[(((((((triple2) -> rule6)) -> rule2) ((triple2) -> rule6)) -> rule3))]
("Charlie" "is" "furry" "-")
((((((triple2) -> (rule6 % int3))) -> (rule2 % int2)) ((triple2) -> (rule6 % int3))) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Bob is not young.
Unknown
inv-rconc
[@3: Bob is young.[CWA. Example of deepest failure = (rule7 <- rule2 <- rule6 <- FAIL)]]
("Bob" "is" "young" "-")
Fiona is young.
Unknown
rconc
[@3: Fiona is young.[CWA. Example of deepest failure = (rule7 <- rule2 <- rule6 <- FAIL)]]
("Fiona" "is" "young" "+")
Bob is not green.
Unknown
inv-rconc
[@3: Bob is green.[CWA. Example of deepest failure = (rule2 <- rule7 <- rule1 <- FAIL)]]
("Bob" "is" "green" "-")
Bob is red.
Unknown
rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Bob" "is" "red" "+")
Bob is not white.
Unknown
inv-random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
@0: Bob is not cold.[(triple1)] Charlie is big.[(triple2)] Fiona is not big.[(triple3)] @1: Charlie is young.[(((triple2) -> rule6))] @2: Charlie is green.[(((((triple2) -> rule6)) -> rule2))] @3: Charlie is furry.[(((((((triple2) -> rule6)) -> rule2) ((triple2) -> rule6)) -> rule3))]
Bob is not cold.
("Bob" "is" "cold" "-")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
triple2
Fiona is not big.
("Fiona" "is" "big" "-")
triple3
Charlie is young.
("Charlie" "is" "young" "+")
((triple2) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
((((((triple2) -> (rule6 % int3))) -> (rule2 % int2)) ((triple2) -> (rule6 % int3))) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3