Bob is furry. Charlie is green. Dave is blue. Dave is cold. Dave is smart. Gary is cold. Gary is furry. If something is furry and green then it is cold. Furry things are green. All green, furry things are cold.
Bob is furry.
("Bob" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
If something is furry and green then it is cold.
((("something" "is" "furry" "+") ("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
Furry things are green.
((("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
All green, furry things are cold.
((("something" "is" "green" "+") ("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
Bob is furry.
True
1
proof
[(triple1)]
("Bob" "is" "furry" "+")
triple1
Dave is not cold.
False
1
inv-proof
[(triple4)]
("Dave" "is" "cold" "-")
triple4
Bob is green.
True
2
proof
[(((triple1) -> rule2))]
("Bob" "is" "green" "+")
((triple1) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Gary is not green.
False
2
inv-proof
[(((triple7) -> rule2))]
("Gary" "is" "green" "-")
((triple7) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Bob is cold.
True
4
proof
[(((triple1 ((triple1) -> rule2)) -> rule1) OR ((((triple1) -> rule2) triple1) -> rule3))]
("Bob" "is" "cold" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((triple1) -> (rule2 % int2)) triple1) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is not cold.
False
4
inv-proof
[(((triple1 ((triple1) -> rule2)) -> rule1) OR ((((triple1) -> rule2) triple1) -> rule3))]
("Bob" "is" "cold" "-")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((triple1) -> (rule2 % int2)) triple1) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Charlie is not cold.
Unknown
inv-rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "cold" "-")
Dave is green.
Unknown
rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "green" "+")
Bob is not smart.
Unknown
inv-random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
@0: Bob is furry.[(triple1)] Charlie is green.[(triple2)] Dave is blue.[(triple3)] Dave is cold.[(triple4)] Dave is smart.[(triple5)] Gary is cold.[(triple6 OR ((triple7 ((triple7) -> rule2)) -> rule1) OR ((((triple7) -> rule2) triple7) -> rule3))] Gary is furry.[(triple7)] @1: Bob is green.[(((triple1) -> rule2))] Gary is green.[(((triple7) -> rule2))] @2: Bob is cold.[(((triple1 ((triple1) -> rule2)) -> rule1) OR ((((triple1) -> rule2) triple1) -> rule3))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Dave is blue.
("Dave" "is" "blue" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
triple4
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Gary is cold.
("Gary" "is" "cold" "+")
triple6
((triple7 ((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((triple7) -> (rule2 % int2)) triple7) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
triple7
Bob is green.
("Bob" "is" "green" "+")
((triple1) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple7) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((triple1) -> (rule2 % int2)) triple1) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2