Bob is kind. Charlie is cold. If Charlie is smart then Charlie is cold. Big people are smart. If someone is cold then they are blue. If someone is kind then they are blue. Blue people are smart. All furry, kind people are big.
Bob is kind.
("Bob" "is" "kind" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
If Charlie is smart then Charlie is cold.
((("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "cold" "+"))
Big people are smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
If someone is cold then they are blue.
((("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
If someone is kind then they are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
Blue people are smart.
((("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
All furry, kind people are big.
((("someone" "is" "furry" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
Charlie is cold.
True
1
proof
[(triple2)]
("Charlie" "is" "cold" "+")
triple2
Charlie is not cold.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "cold" "-")
triple2
Charlie is blue.
True
2
proof
[(((triple2) -> rule3))]
("Charlie" "is" "blue" "+")
((triple2) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is not blue.
False
2
inv-proof
[(((triple2) -> rule3))]
("Charlie" "is" "blue" "-")
((triple2) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is not big.
Unknown
inv-rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "big" "-")
Bob is big.
Unknown
rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "big" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Bob is kind.[(triple1)] Charlie is cold.[(triple2)] @1: Bob is blue.[(((triple1) -> rule4))] Charlie is blue.[(((triple2) -> rule3))] @2: Bob is smart.[(((((triple1) -> rule4)) -> rule5))] Charlie is smart.[(((((triple2) -> rule3)) -> rule5))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Bob is blue.
("Bob" "is" "blue" "+")
((triple1) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple2) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2