Bob is smart. Dave is furry. Gary is green. Blue things are not smart. Furry things are smart. Blue things are smart. All smart things are green. If Gary is blue and Gary is smart then Gary is green. Green things are red. Blue, cold things are not red. If something is kind and not smart then it is cold.
Bob is smart.
("Bob" "is" "smart" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Blue things are not smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "-"))
Furry things are smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
Blue things are smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
All smart things are green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
If Gary is blue and Gary is smart then Gary is green.
((("Gary" "is" "blue" "+") ("Gary" "is" "smart" "+")) -> ("Gary" "is" "green" "+"))
Green things are red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
Blue, cold things are not red.
((("something" "is" "blue" "+") ("something" "is" "cold" "+")) -> ("something" "is" "red" "-"))
If something is kind and not smart then it is cold.
((("something" "is" "kind" "+") ("something" "is" "smart" "~")) -> ("something" "is" "cold" "+"))
Dave is furry.
True
1
proof
[(triple2)]
("Dave" "is" "furry" "+")
triple2
Gary is not green.
False
1
inv-proof
[(triple3)]
("Gary" "is" "green" "-")
triple3
Bob is green.
True
2
proof
[(((triple1) -> rule4))]
("Bob" "is" "green" "+")
((triple1) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is not green.
False
2
inv-proof
[(((triple1) -> rule4))]
("Bob" "is" "green" "-")
((triple1) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is red.
True
3
proof
[(((((triple1) -> rule4)) -> rule6))]
("Bob" "is" "red" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is not red.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule6))]
("Bob" "is" "red" "-")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Dave is red.
True
4
proof
[(((((((triple2) -> rule2)) -> rule4)) -> rule6))]
("Dave" "is" "red" "+")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is not red.
False
4
inv-proof
[(((((((triple2) -> rule2)) -> rule4)) -> rule6))]
("Dave" "is" "red" "-")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Gary is not cold.
Unknown
inv-rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Gary" "is" "cold" "-")
Dave is cold.
Unknown
rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "cold" "+")
Gary is not smart.
Unknown
inv-rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "smart" "-")
Bob is cold.
Unknown
rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Bob" "is" "cold" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
@0: Bob is smart.[(triple1)] Dave is furry.[(triple2)] Gary is green.[(triple3)] @1: Bob is green.[(((triple1) -> rule4))] Dave is smart.[(((triple2) -> rule2))] Gary is red.[(((triple3) -> rule6))] @2: Bob is red.[(((((triple1) -> rule4)) -> rule6))] Dave is green.[(((((triple2) -> rule2)) -> rule4))] @3: Dave is red.[(((((((triple2) -> rule2)) -> rule4)) -> rule6))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Gary is green.
("Gary" "is" "green" "+")
triple3
Bob is green.
("Bob" "is" "green" "+")
((triple1) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple2) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple3) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3