Bob is red. Bob is smart. Charlie is red. Charlie is white. Dave is rough. Gary is not big. Gary is red. All white people are not blue. Rough people are not blue. If someone is rough and not smart then they are not red. All white people are red. All rough people are not red. Big people are not red. Red people are white. If Gary is big then Gary is nice.
Bob is red.
("Bob" "is" "red" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Gary is not big.
("Gary" "is" "big" "-")
Gary is red.
("Gary" "is" "red" "+")
All white people are not blue.
((("someone" "is" "white" "+")) -> ("someone" "is" "blue" "-"))
Rough people are not blue.
((("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "-"))
If someone is rough and not smart then they are not red.
((("someone" "is" "rough" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "red" "-"))
All white people are red.
((("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
All rough people are not red.
((("someone" "is" "rough" "+")) -> ("someone" "is" "red" "-"))
Big people are not red.
((("someone" "is" "big" "+")) -> ("someone" "is" "red" "-"))
Red people are white.
((("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
If Gary is big then Gary is nice.
((("Gary" "is" "big" "+")) -> ("Gary" "is" "nice" "+"))
Gary is red.
True
1
proof
[(triple7)]
("Gary" "is" "red" "+")
triple7
Bob is not red.
False
1
inv-proof
[(triple1)]
("Bob" "is" "red" "-")
triple1
Dave is not blue.
True
2
proof
[(((triple5) -> rule2))]
("Dave" "is" "blue" "-")
((triple5) -> (rule2 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is red.
False
2
inv-proof
[(((triple5) -> rule5))]
("Dave" "is" "red" "+")
((triple5) -> (rule5 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Bob is not blue.
True
3
proof
[(((((triple1) -> rule7)) -> rule1))]
("Bob" "is" "blue" "-")
((((triple1) -> (rule7 % int2))) -> (rule1 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Gary is blue.
False
3
inv-proof
[(((((triple7) -> rule7)) -> rule1))]
("Gary" "is" "blue" "+")
((((triple7) -> (rule7 % int2))) -> (rule1 % int1))
Gary is not blue.
("Gary" "is" "blue" "-")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is not nice.
Unknown
inv-rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Gary" "is" "nice" "-")
Dave is white.
Unknown
rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "white" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Bob is red.[(triple1)] Bob is smart.[(triple2)] Charlie is red.[(triple3 OR ((triple4) -> rule4))] Charlie is white.[(triple4 OR ((triple3) -> rule7))] Dave is rough.[(triple5)] Gary is not big.[(triple6)] Gary is red.[(triple7)] @1: Bob is white.[(((triple1) -> rule7))] Charlie is not blue.[(((triple4) -> rule1) OR ((((triple3) -> rule7)) -> rule1))] Dave is not blue.[(((triple5) -> rule2))] Dave is not red.[(((triple5) -> rule5))] Gary is white.[(((triple7) -> rule7))] @2: Bob is not blue.[(((((triple1) -> rule7)) -> rule1))] Gary is not blue.[(((((triple7) -> rule7)) -> rule1))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Charlie is red.
("Charlie" "is" "red" "+")
triple3
((triple4) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
triple4
((triple3) -> (rule7 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple5
Gary is not big.
("Gary" "is" "big" "-")
triple6
Gary is red.
("Gary" "is" "red" "+")
triple7
Bob is white.
("Bob" "is" "white" "+")
((triple1) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Charlie is not blue.
("Charlie" "is" "blue" "-")
((triple4) -> (rule1 % int1))
Charlie is not blue.
("Charlie" "is" "blue" "-")
int1
((((triple3) -> (rule7 % int2))) -> (rule1 % int1))
Charlie is not blue.
("Charlie" "is" "blue" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Dave is not blue.
("Dave" "is" "blue" "-")
((triple5) -> (rule2 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is not red.
("Dave" "is" "red" "-")
((triple5) -> (rule5 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple7) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Bob is not blue.
("Bob" "is" "blue" "-")
((((triple1) -> (rule7 % int2))) -> (rule1 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Gary is not blue.
("Gary" "is" "blue" "-")
((((triple7) -> (rule7 % int2))) -> (rule1 % int1))
Gary is not blue.
("Gary" "is" "blue" "-")
int1
Gary is white.
("Gary" "is" "white" "+")
int2