Bob is red. Erin is not nice. Erin is red. Gary is big. Gary is not green. Gary is red. Gary is rough. Harry is red. Harry is rough. Harry is white. All rough things are not nice. If something is red and white then it is not nice. Big, red things are quiet. All quiet, big things are white. If something is quiet and not white then it is green. If something is nice and not red then it is green.
Bob is red.
("Bob" "is" "red" "+")
Erin is not nice.
("Erin" "is" "nice" "-")
Erin is red.
("Erin" "is" "red" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is not green.
("Gary" "is" "green" "-")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is white.
("Harry" "is" "white" "+")
All rough things are not nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "-"))
If something is red and white then it is not nice.
((("something" "is" "red" "+") ("something" "is" "white" "+")) -> ("something" "is" "nice" "-"))
Big, red things are quiet.
((("something" "is" "big" "+") ("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
All quiet, big things are white.
((("something" "is" "quiet" "+") ("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
If something is quiet and not white then it is green.
((("something" "is" "quiet" "+") ("something" "is" "white" "~")) -> ("something" "is" "green" "+"))
If something is nice and not red then it is green.
((("something" "is" "nice" "+") ("something" "is" "red" "~")) -> ("something" "is" "green" "+"))
Gary is not green.
True
1
proof
[(triple5)]
("Gary" "is" "green" "-")
triple5
Bob is not red.
False
1
inv-proof
[(triple1)]
("Bob" "is" "red" "-")
triple1
Gary is quiet.
True
3
proof
[(((triple4 triple6) -> rule3))]
("Gary" "is" "quiet" "+")
((triple4 triple6) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Harry is nice.
False
2
inv-proof
[(((triple9) -> rule1) OR ((triple8 triple10) -> rule2))]
("Harry" "is" "nice" "+")
((triple9) -> (rule1 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
((triple8 triple10) -> (rule2 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Gary is white.
True
5
proof
[(((((triple4 triple6) -> rule3) triple4) -> rule4))]
("Gary" "is" "white" "+")
((((triple4 triple6) -> (rule3 % int2)) triple4) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is not white.
False
5
inv-proof
[(((((triple4 triple6) -> rule3) triple4) -> rule4))]
("Gary" "is" "white" "-")
((((triple4 triple6) -> (rule3 % int2)) triple4) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Erin is not white.
Unknown
inv-rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "white" "-")
Harry is green.
Unknown
rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "green" "+")
Bob is not green.
Unknown
inv-rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "green" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
Erin is not rough.
Unknown
inv-random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
@0: Bob is red.[(triple1)] Erin is not nice.[(triple2)] Erin is red.[(triple3)] Gary is big.[(triple4)] Gary is not green.[(triple5)] Gary is red.[(triple6)] Gary is rough.[(triple7)] Harry is red.[(triple8)] Harry is rough.[(triple9)] Harry is white.[(triple10)] @1: Gary is not nice.[(((triple7) -> rule1) OR ((triple6 ((((triple4 triple6) -> rule3) triple4) -> rule4)) -> rule2))] Gary is quiet.[(((triple4 triple6) -> rule3))] Harry is not nice.[(((triple9) -> rule1) OR ((triple8 triple10) -> rule2))] @2: Gary is white.[(((((triple4 triple6) -> rule3) triple4) -> rule4))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Erin is not nice.
("Erin" "is" "nice" "-")
triple2
Erin is red.
("Erin" "is" "red" "+")
triple3
Gary is big.
("Gary" "is" "big" "+")
triple4
Gary is not green.
("Gary" "is" "green" "-")
triple5
Gary is red.
("Gary" "is" "red" "+")
triple6
Gary is rough.
("Gary" "is" "rough" "+")
triple7
Harry is red.
("Harry" "is" "red" "+")
triple8
Harry is rough.
("Harry" "is" "rough" "+")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple10
Gary is not nice.
("Gary" "is" "nice" "-")
((triple7) -> (rule1 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
((triple6 ((((triple4 triple6) -> (rule3 % int3)) triple4) -> (rule4 % int2))) -> (rule2 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple4 triple6) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Harry is not nice.
("Harry" "is" "nice" "-")
((triple9) -> (rule1 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
((triple8 triple10) -> (rule2 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Gary is white.
("Gary" "is" "white" "+")
((((triple4 triple6) -> (rule3 % int2)) triple4) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2