Bob is smart. Bob is young. Dave is young. All red things are cold. All green things are cold. If something is white and kind then it is green. If something is red and smart then it is kind. Young things are white. If something is smart and young then it is red.
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is young.
("Dave" "is" "young" "+")
All red things are cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
All green things are cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
If something is white and kind then it is green.
((("something" "is" "white" "+") ("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
If something is red and smart then it is kind.
((("something" "is" "red" "+") ("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
Young things are white.
((("something" "is" "young" "+")) -> ("something" "is" "white" "+"))
If something is smart and young then it is red.
((("something" "is" "smart" "+") ("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
Bob is young.
True
1
proof
[(triple2)]
("Bob" "is" "young" "+")
triple2
Bob is not young.
False
1
inv-proof
[(triple2)]
("Bob" "is" "young" "-")
triple2
Bob is white.
True
2
proof
[(((triple2) -> rule5))]
("Bob" "is" "white" "+")
((triple2) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Dave is not white.
False
2
inv-proof
[(((triple3) -> rule5))]
("Dave" "is" "white" "-")
((triple3) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Bob is cold.
True
4
proof
[(((((triple1 triple2) -> rule6)) -> rule1) OR ((((((triple2) -> rule5) ((((triple1 triple2) -> rule6) triple1) -> rule4)) -> rule3)) -> rule2))]
("Bob" "is" "cold" "+")
((((triple1 triple2) -> (rule6 % int2))) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((((((triple2) -> (rule5 % int5)) ((((triple1 triple2) -> (rule6 % int4)) triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
Bob is white.
("Bob" "is" "white" "+")
int5
Bob is not kind.
False
5
inv-proof
[(((((triple1 triple2) -> rule6) triple1) -> rule4))]
("Bob" "is" "kind" "-")
((((triple1 triple2) -> (rule6 % int2)) triple1) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is green.
True
8
proof
[(((((triple2) -> rule5) ((((triple1 triple2) -> rule6) triple1) -> rule4)) -> rule3))]
("Bob" "is" "green" "+")
((((triple2) -> (rule5 % int4)) ((((triple1 triple2) -> (rule6 % int3)) triple1) -> (rule4 % int2))) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is not green.
False
8
inv-proof
[(((((triple2) -> rule5) ((((triple1 triple2) -> rule6) triple1) -> rule4)) -> rule3))]
("Bob" "is" "green" "-")
((((triple2) -> (rule5 % int4)) ((((triple1 triple2) -> (rule6 % int3)) triple1) -> (rule4 % int2))) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Dave is not kind.
Unknown
inv-rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "kind" "-")
Dave is green.
Unknown
rconc
[@2: Dave is green.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Dave" "is" "green" "+")
Dave is not red.
Unknown
inv-rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "red" "-")
Dave is cold.
Unknown
rconc
[@3: Dave is cold.[CWA. Example of deepest failure = (rule2 <- rule3 <- rule4 <- FAIL)]]
("Dave" "is" "cold" "+")
@0: Bob is smart.[(triple1)] Bob is young.[(triple2)] Dave is young.[(triple3)] @1: Bob is red.[(((triple1 triple2) -> rule6))] Bob is white.[(((triple2) -> rule5))] Dave is white.[(((triple3) -> rule5))] @2: Bob is cold.[(((((triple1 triple2) -> rule6)) -> rule1) OR ((((((triple2) -> rule5) ((((triple1 triple2) -> rule6) triple1) -> rule4)) -> rule3)) -> rule2))] Bob is kind.[(((((triple1 triple2) -> rule6) triple1) -> rule4))] @3: Bob is green.[(((((triple2) -> rule5) ((((triple1 triple2) -> rule6) triple1) -> rule4)) -> rule3))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Bob is young.
("Bob" "is" "young" "+")
triple2
Dave is young.
("Dave" "is" "young" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
((triple1 triple2) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((triple2) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((triple3) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((((triple1 triple2) -> (rule6 % int2))) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((((((triple2) -> (rule5 % int5)) ((((triple1 triple2) -> (rule6 % int4)) triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
Bob is white.
("Bob" "is" "white" "+")
int5
Bob is kind.
("Bob" "is" "kind" "+")
((((triple1 triple2) -> (rule6 % int2)) triple1) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
((((triple2) -> (rule5 % int4)) ((((triple1 triple2) -> (rule6 % int3)) triple1) -> (rule4 % int2))) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4