Bob is kind. Bob is round. Bob is white. Bob is not young. Charlie is blue. Charlie is smart. Erin is round. All round, white things are smart. Smart things are not cold.
Bob is kind.
("Bob" "is" "kind" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is not young.
("Bob" "is" "young" "-")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Erin is round.
("Erin" "is" "round" "+")
All round, white things are smart.
((("something" "is" "round" "+") ("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
Smart things are not cold.
((("something" "is" "smart" "+")) -> ("something" "is" "cold" "-"))
Bob is round.
True
1
proof
[(triple2)]
("Bob" "is" "round" "+")
triple2
Bob is young.
False
1
inv-proof
[(triple4)]
("Bob" "is" "young" "+")
triple4
Bob is smart.
True
3
proof
[(((triple2 triple3) -> rule1))]
("Bob" "is" "smart" "+")
((triple2 triple3) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Charlie is cold.
False
2
inv-proof
[(((triple6) -> rule2))]
("Charlie" "is" "cold" "+")
((triple6) -> (rule2 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Bob is not cold.
True
4
proof
[(((((triple2 triple3) -> rule1)) -> rule2))]
("Bob" "is" "cold" "-")
((((triple2 triple3) -> (rule1 % int2))) -> (rule2 % int1))
Bob is not cold.
("Bob" "is" "cold" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is cold.
False
4
inv-proof
[(((((triple2 triple3) -> rule1)) -> rule2))]
("Bob" "is" "cold" "+")
((((triple2 triple3) -> (rule1 % int2))) -> (rule2 % int1))
Bob is not cold.
("Bob" "is" "cold" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Erin is not smart.
Unknown
inv-rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "smart" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
Erin is not young.
Unknown
inv-random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
@0: Bob is kind.[(triple1)] Bob is not young.[(triple4)] Bob is round.[(triple2)] Bob is white.[(triple3)] Charlie is blue.[(triple5)] Charlie is smart.[(triple6)] Erin is round.[(triple7)] @1: Bob is smart.[(((triple2 triple3) -> rule1))] Charlie is not cold.[(((triple6) -> rule2))] @2: Bob is not cold.[(((((triple2 triple3) -> rule1)) -> rule2))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Bob is not young.
("Bob" "is" "young" "-")
triple4
Bob is round.
("Bob" "is" "round" "+")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple3
Charlie is blue.
("Charlie" "is" "blue" "+")
triple5
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
Erin is round.
("Erin" "is" "round" "+")
triple7
Bob is smart.
("Bob" "is" "smart" "+")
((triple2 triple3) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Charlie is not cold.
("Charlie" "is" "cold" "-")
((triple6) -> (rule2 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Bob is not cold.
("Bob" "is" "cold" "-")
((((triple2 triple3) -> (rule1 % int2))) -> (rule2 % int1))
Bob is not cold.
("Bob" "is" "cold" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2