Bob is big. Charlie is nice. Dave is nice. Gary is nice. If Dave is green and Dave is rough then Dave is white. Nice, blue people are white. All smart, nice people are blue. If someone is rough then they are smart. Rough people are nice. If someone is nice then they are rough. Blue people are smart. If Bob is rough and Bob is nice then Bob is blue.
Bob is big.
("Bob" "is" "big" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Gary is nice.
("Gary" "is" "nice" "+")
If Dave is green and Dave is rough then Dave is white.
((("Dave" "is" "green" "+") ("Dave" "is" "rough" "+")) -> ("Dave" "is" "white" "+"))
Nice, blue people are white.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
All smart, nice people are blue.
((("someone" "is" "smart" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
If someone is rough then they are smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
Rough people are nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
If someone is nice then they are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
Blue people are smart.
((("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
If Bob is rough and Bob is nice then Bob is blue.
((("Bob" "is" "rough" "+") ("Bob" "is" "nice" "+")) -> ("Bob" "is" "blue" "+"))
Gary is nice.
True
1
proof
[(triple4)]
("Gary" "is" "nice" "+")
triple4
Gary is not nice.
False
1
inv-proof
[(triple4)]
("Gary" "is" "nice" "-")
triple4
Dave is rough.
True
2
proof
[(((triple3) -> rule6))]
("Dave" "is" "rough" "+")
((triple3) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Gary is not rough.
False
2
inv-proof
[(((triple4) -> rule6))]
("Gary" "is" "rough" "-")
((triple4) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is smart.
True
3
proof
[(((((triple4) -> rule6)) -> rule4))]
("Gary" "is" "smart" "+")
((((triple4) -> (rule6 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Charlie is not smart.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule4))]
("Charlie" "is" "smart" "-")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is blue.
True
5
proof
[(((((((triple2) -> rule6)) -> rule4) triple2) -> rule3))]
("Charlie" "is" "blue" "+")
((((((triple2) -> (rule6 % int3))) -> (rule4 % int2)) triple2) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Gary is not blue.
False
5
inv-proof
[(((((((triple4) -> rule6)) -> rule4) triple4) -> rule3))]
("Gary" "is" "blue" "-")
((((((triple4) -> (rule6 % int3))) -> (rule4 % int2)) triple4) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Bob is not white.
Unknown
inv-rconc
[@3: Bob is white.[CWA. Example of deepest failure = (rule2 <- rule5 <- rule6 <- FAIL)]]
("Bob" "is" "white" "-")
Bob is smart.
Unknown
rconc
[@4: Bob is smart.[CWA. Example of deepest failure = (rule7 <- rule3 <- rule5 <- rule6 <- FAIL)]]
("Bob" "is" "smart" "+")
Bob is not blue.
Unknown
inv-rconc
[@3: Bob is blue.[CWA. Example of deepest failure = (rule3 <- rule5 <- rule6 <- FAIL)]]
("Bob" "is" "blue" "-")
Bob is rough.
Unknown
rconc
[@2: Bob is rough.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("Bob" "is" "rough" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
@0: Bob is big.[(triple1)] Charlie is nice.[(triple2)] Dave is nice.[(triple3)] Gary is nice.[(triple4)] @1: Charlie is rough.[(((triple2) -> rule6))] Dave is rough.[(((triple3) -> rule6))] Gary is rough.[(((triple4) -> rule6))] @2: Charlie is smart.[(((((triple2) -> rule6)) -> rule4))] Dave is smart.[(((((triple3) -> rule6)) -> rule4))] Gary is smart.[(((((triple4) -> rule6)) -> rule4))] @3: Charlie is blue.[(((((((triple2) -> rule6)) -> rule4) triple2) -> rule3))] Dave is blue.[(((((((triple3) -> rule6)) -> rule4) triple3) -> rule3))] Gary is blue.[(((((((triple4) -> rule6)) -> rule4) triple4) -> rule3))] @4: Charlie is white.[(((triple2 ((((((triple2) -> rule6)) -> rule4) triple2) -> rule3)) -> rule2))] Dave is white.[(((triple3 ((((((triple3) -> rule6)) -> rule4) triple3) -> rule3)) -> rule2))] Gary is white.[(((triple4 ((((((triple4) -> rule6)) -> rule4) triple4) -> rule3)) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Gary is nice.
("Gary" "is" "nice" "+")
triple4
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple2) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple3) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple4) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((((triple3) -> (rule6 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((((triple4) -> (rule6 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
((((((triple2) -> (rule6 % int3))) -> (rule4 % int2)) triple2) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
((((((triple3) -> (rule6 % int3))) -> (rule4 % int2)) triple3) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
((((((triple4) -> (rule6 % int3))) -> (rule4 % int2)) triple4) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
((triple2 ((((((triple2) -> (rule6 % int4))) -> (rule4 % int3)) triple2) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
int4
Dave is white.
("Dave" "is" "white" "+")
((triple3 ((((((triple3) -> (rule6 % int4))) -> (rule4 % int3)) triple3) -> (rule3 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Gary is white.
("Gary" "is" "white" "+")
((triple4 ((((((triple4) -> (rule6 % int4))) -> (rule4 % int3)) triple4) -> (rule3 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
int4