Bob is young. Gary is young. Harry is kind. If something is cold and red then it is kind. If something is red then it is blue. All young things are red. Kind, blue things are quiet. All blue things are not round. If Gary is not red and Gary is not young then Gary is quiet.
Bob is young.
("Bob" "is" "young" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is kind.
("Harry" "is" "kind" "+")
If something is cold and red then it is kind.
((("something" "is" "cold" "+") ("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
If something is red then it is blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
All young things are red.
((("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
Kind, blue things are quiet.
((("something" "is" "kind" "+") ("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
All blue things are not round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "-"))
If Gary is not red and Gary is not young then Gary is quiet.
((("Gary" "is" "red" "~") ("Gary" "is" "young" "~")) -> ("Gary" "is" "quiet" "+"))
Bob is young.
True
1
proof
[(triple1)]
("Bob" "is" "young" "+")
triple1
Bob is not young.
False
1
inv-proof
[(triple1)]
("Bob" "is" "young" "-")
triple1
Bob is red.
True
2
proof
[(((triple1) -> rule3))]
("Bob" "is" "red" "+")
((triple1) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Gary is not red.
False
2
inv-proof
[(((triple2) -> rule3))]
("Gary" "is" "red" "-")
((triple2) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is blue.
True
3
proof
[(((((triple2) -> rule3)) -> rule2))]
("Gary" "is" "blue" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is not blue.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule2))]
("Gary" "is" "blue" "-")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is not round.
True
4
proof
[(((((((triple2) -> rule3)) -> rule2)) -> rule5))]
("Gary" "is" "round" "-")
((((((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Gary is not round.
("Gary" "is" "round" "-")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Bob is round.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule2)) -> rule5))]
("Bob" "is" "round" "+")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Bob is not round.
("Bob" "is" "round" "-")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Harry is not blue.
Unknown
inv-rconc
[@2: Harry is blue.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Harry" "is" "blue" "-")
Gary is kind.
Unknown
rconc
[@1: Gary is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "kind" "+")
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "red" "-")
Harry is quiet.
Unknown
rconc
[@3: Harry is quiet.[CWA. Example of deepest failure = (rule4 <- rule2 <- rule3 <- FAIL)]]
("Harry" "is" "quiet" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
@0: Bob is young.[(triple1)] Gary is young.[(triple2)] Harry is kind.[(triple3)] @1: Bob is red.[(((triple1) -> rule3))] Gary is red.[(((triple2) -> rule3))] @2: Bob is blue.[(((((triple1) -> rule3)) -> rule2))] Gary is blue.[(((((triple2) -> rule3)) -> rule2))] @3: Bob is not round.[(((((((triple1) -> rule3)) -> rule2)) -> rule5))] Gary is not round.[(((((((triple2) -> rule3)) -> rule2)) -> rule5))]
Bob is young.
("Bob" "is" "young" "+")
triple1
Gary is young.
("Gary" "is" "young" "+")
triple2
Harry is kind.
("Harry" "is" "kind" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
((triple1) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple2) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Bob is not round.
("Bob" "is" "round" "-")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Bob is not round.
("Bob" "is" "round" "-")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Gary is not round.
("Gary" "is" "round" "-")
((((((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Gary is not round.
("Gary" "is" "round" "-")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3