Bob is blue. Bob is not cold. Bob is red. Charlie is kind. Charlie is not rough. Gary is not cold. Harry is red. If someone is smart and not cold then they are kind. If someone is quiet then they are kind. All rough people are blue. Rough, kind people are blue. If Bob is blue and Bob is kind then Bob is rough. All red, rough people are quiet. All red, blue people are rough. Blue people are rough.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is not cold.
("Bob" "is" "cold" "-")
Bob is red.
("Bob" "is" "red" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is not rough.
("Charlie" "is" "rough" "-")
Gary is not cold.
("Gary" "is" "cold" "-")
Harry is red.
("Harry" "is" "red" "+")
If someone is smart and not cold then they are kind.
((("someone" "is" "smart" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "kind" "+"))
If someone is quiet then they are kind.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
All rough people are blue.
((("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
Rough, kind people are blue.
((("someone" "is" "rough" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If Bob is blue and Bob is kind then Bob is rough.
((("Bob" "is" "blue" "+") ("Bob" "is" "kind" "+")) -> ("Bob" "is" "rough" "+"))
All red, rough people are quiet.
((("someone" "is" "red" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
All red, blue people are rough.
((("someone" "is" "red" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
Blue people are rough.
((("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
Harry is red.
True
1
proof
[(triple7)]
("Harry" "is" "red" "+")
triple7
Bob is cold.
False
1
inv-proof
[(triple2)]
("Bob" "is" "cold" "+")
triple2
Bob is rough.
True
2
proof
[(((triple1) -> rule8) OR ((triple3 triple1) -> rule7))]
("Bob" "is" "rough" "+")
((triple1) -> (rule8 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((triple3 triple1) -> (rule7 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is not rough.
False
2
inv-proof
[(((triple1) -> rule8) OR ((triple3 triple1) -> rule7))]
("Bob" "is" "rough" "-")
((triple1) -> (rule8 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((triple3 triple1) -> (rule7 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is quiet.
True
4
proof
[(((triple3 ((triple1) -> rule8)) -> rule6) OR ((triple3 ((triple3 triple1) -> rule7)) -> rule6))]
("Bob" "is" "quiet" "+")
((triple3 ((triple1) -> (rule8 % int2))) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((triple3 ((triple3 triple1) -> (rule7 % int2))) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is not quiet.
False
4
inv-proof
[(((triple3 ((triple1) -> rule8)) -> rule6) OR ((triple3 ((triple3 triple1) -> rule7)) -> rule6))]
("Bob" "is" "quiet" "-")
((triple3 ((triple1) -> (rule8 % int2))) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((triple3 ((triple3 triple1) -> (rule7 % int2))) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is kind.
True
5
proof
[(((((triple3 ((triple1) -> rule8)) -> rule6)) -> rule2) OR ((((triple3 ((triple3 triple1) -> rule7)) -> rule6)) -> rule2))]
("Bob" "is" "kind" "+")
((((triple3 ((triple1) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
((((triple3 ((triple3 triple1) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is not kind.
False
5
inv-proof
[(((((triple3 ((triple1) -> rule8)) -> rule6)) -> rule2) OR ((((triple3 ((triple3 triple1) -> rule7)) -> rule6)) -> rule2))]
("Bob" "is" "kind" "-")
((((triple3 ((triple1) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
((((triple3 ((triple3 triple1) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Gary is not rough.
Unknown
inv-rconc
[@3: Gary is rough.[CWA. Example of deepest failure = (rule8 <- rule3 <- rule7 <- FAIL)]]
("Gary" "is" "rough" "-")
Harry is kind.
Unknown
rconc
[@6: Harry is kind.[CWA. Example of deepest failure = (rule2 <- rule6 <- rule7 <- rule3 <- rule8 <- rule4 <- FAIL)]]
("Harry" "is" "kind" "+")
Gary is not blue.
Unknown
inv-rconc
[@4: Gary is blue.[CWA. Example of deepest failure = (rule3 <- rule8 <- rule4 <- rule7 <- FAIL)]]
("Gary" "is" "blue" "-")
Harry is blue.
Unknown
rconc
[@4: Harry is blue.[CWA. Example of deepest failure = (rule3 <- rule7 <- rule4 <- rule8 <- FAIL)]]
("Harry" "is" "blue" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
@0: Bob is blue.[(triple1)] Bob is not cold.[(triple2)] Bob is red.[(triple3)] Charlie is kind.[(triple4)] Charlie is not rough.[(triple5)] Gary is not cold.[(triple6)] Harry is red.[(triple7)] @1: Bob is rough.[(((triple1) -> rule8) OR ((triple3 triple1) -> rule7))] @2: Bob is quiet.[(((triple3 ((triple1) -> rule8)) -> rule6) OR ((triple3 ((triple3 triple1) -> rule7)) -> rule6))] @3: Bob is kind.[(((((triple3 ((triple1) -> rule8)) -> rule6)) -> rule2) OR ((((triple3 ((triple3 triple1) -> rule7)) -> rule6)) -> rule2))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is not cold.
("Bob" "is" "cold" "-")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Charlie is not rough.
("Charlie" "is" "rough" "-")
triple5
Gary is not cold.
("Gary" "is" "cold" "-")
triple6
Harry is red.
("Harry" "is" "red" "+")
triple7
Bob is rough.
("Bob" "is" "rough" "+")
((triple1) -> (rule8 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((triple3 triple1) -> (rule7 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple3 ((triple1) -> (rule8 % int2))) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((triple3 ((triple3 triple1) -> (rule7 % int2))) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
((((triple3 ((triple1) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
((((triple3 ((triple3 triple1) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3