Anne is blue. Anne is round. Bob is blue. Bob is smart. Charlie is kind. Charlie is smart. Gary is cold. Round, kind things are smart. Cold things are smart. All young, blue things are cold. If Charlie is cold then Charlie is young. Blue things are round. All smart things are blue.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is round.
("Anne" "is" "round" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Round, kind things are smart.
((("something" "is" "round" "+") ("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
Cold things are smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
All young, blue things are cold.
((("something" "is" "young" "+") ("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
If Charlie is cold then Charlie is young.
((("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "young" "+"))
Blue things are round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
All smart things are blue.
((("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
Bob is smart.
True
1
proof
[(triple4)]
("Bob" "is" "smart" "+")
triple4
Gary is not cold.
False
1
inv-proof
[(triple7)]
("Gary" "is" "cold" "-")
triple7
Charlie is blue.
True
2
proof
[(((triple6) -> rule6))]
("Charlie" "is" "blue" "+")
((triple6) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is not blue.
False
2
inv-proof
[(((triple6) -> rule6))]
("Charlie" "is" "blue" "-")
((triple6) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is round.
True
3
proof
[(((((triple6) -> rule6)) -> rule5))]
("Charlie" "is" "round" "+")
((((triple6) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is not round.
False
3
inv-proof
[(((((triple6) -> rule6)) -> rule5))]
("Charlie" "is" "round" "-")
((((triple6) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is not young.
Unknown
inv-rconc
[@2: Charlie is young.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("Charlie" "is" "young" "-")
Anne is smart.
Unknown
rconc
[@2: Anne is smart.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Anne" "is" "smart" "+")
Charlie is not cold.
Unknown
inv-rconc
[@2: Charlie is cold.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Charlie" "is" "cold" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Anne is blue.[(triple1)] Anne is round.[(triple2 OR ((triple1) -> rule5))] Bob is blue.[(triple3 OR ((triple4) -> rule6))] Bob is smart.[(triple4)] Charlie is kind.[(triple5)] Charlie is smart.[(triple6)] Gary is cold.[(triple7)] @1: Bob is round.[(((triple3) -> rule5) OR ((((triple4) -> rule6)) -> rule5))] Charlie is blue.[(((triple6) -> rule6))] Gary is smart.[(((triple7) -> rule2))] @2: Charlie is round.[(((((triple6) -> rule6)) -> rule5))] Gary is blue.[(((((triple7) -> rule2)) -> rule6))] @3: Gary is round.[(((((((triple7) -> rule2)) -> rule6)) -> rule5))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
((triple1) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
triple3
((triple4) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
triple4
Charlie is kind.
("Charlie" "is" "kind" "+")
triple5
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
Gary is cold.
("Gary" "is" "cold" "+")
triple7
Bob is round.
("Bob" "is" "round" "+")
((triple3) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((((triple4) -> (rule6 % int2))) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple6) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple7) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((((triple6) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((((triple7) -> (rule2 % int2))) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
((((((triple7) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3