Bob is blue. Bob is round. Bob is smart. Bob is white. Charlie is blue. Charlie is green. Charlie is nice. Charlie is rough. Charlie is round. Charlie is smart. Gary is blue. Gary is round. Harry is blue. Harry is nice. Harry is smart. All green, blue people are round. All smart people are nice. If Bob is nice then Bob is rough. If someone is smart then they are rough. All rough people are green. If Harry is round and Harry is nice then Harry is smart.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All green, blue people are round.
((("someone" "is" "green" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
All smart people are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
If Bob is nice then Bob is rough.
((("Bob" "is" "nice" "+")) -> ("Bob" "is" "rough" "+"))
If someone is smart then they are rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
All rough people are green.
((("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
If Harry is round and Harry is nice then Harry is smart.
((("Harry" "is" "round" "+") ("Harry" "is" "nice" "+")) -> ("Harry" "is" "smart" "+"))
Harry is blue.
True
1
proof
[(triple13)]
("Harry" "is" "blue" "+")
triple13
Charlie is not green.
False
1
inv-proof
[(triple6 OR ((triple8) -> rule5) OR ((((triple10) -> rule4)) -> rule5))]
("Charlie" "is" "green" "-")
triple6
((triple8) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((((triple10) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Bob is rough.
True
2
proof
[(((triple3) -> rule4) OR ((((triple3) -> rule2)) -> rule3))]
("Bob" "is" "rough" "+")
((triple3) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Harry is not rough.
False
2
inv-proof
[(((triple15) -> rule4))]
("Harry" "is" "rough" "-")
((triple15) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Bob is green.
True
3
proof
[(((((triple3) -> rule4)) -> rule5) OR ((((((triple3) -> rule2)) -> rule3)) -> rule5))]
("Bob" "is" "green" "+")
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is not green.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule5) OR ((((((triple3) -> rule2)) -> rule3)) -> rule5))]
("Bob" "is" "green" "-")
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Harry is round.
True
5
proof
[(((((((triple15) -> rule4)) -> rule5) triple13) -> rule1))]
("Harry" "is" "round" "+")
((((((triple15) -> (rule4 % int3))) -> (rule5 % int2)) triple13) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is not round.
False
5
inv-proof
[(((((((triple15) -> rule4)) -> rule5) triple13) -> rule1))]
("Harry" "is" "round" "-")
((((((triple15) -> (rule4 % int3))) -> (rule5 % int2)) triple13) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Gary is not nice.
Unknown
inv-rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "nice" "-")
Gary is rough.
Unknown
rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "rough" "+")
Gary is not green.
Unknown
inv-rconc
[@2: Gary is green.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Gary" "is" "green" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
@0: Bob is blue.[(triple1)] Bob is round.[(triple2 OR ((((((triple3) -> rule4)) -> rule5) triple1) -> rule1) OR ((((((((triple3) -> rule2)) -> rule3)) -> rule5) triple1) -> rule1))] Bob is smart.[(triple3)] Bob is white.[(triple4)] Charlie is blue.[(triple5)] Charlie is green.[(triple6 OR ((triple8) -> rule5) OR ((((triple10) -> rule4)) -> rule5))] Charlie is nice.[(triple7 OR ((triple10) -> rule2))] Charlie is rough.[(triple8 OR ((triple10) -> rule4))] Charlie is round.[(triple9 OR ((triple6 triple5) -> rule1) OR ((((triple8) -> rule5) triple5) -> rule1) OR ((((((triple10) -> rule4)) -> rule5) triple5) -> rule1))] Charlie is smart.[(triple10)] Gary is blue.[(triple11)] Gary is round.[(triple12)] Harry is blue.[(triple13)] Harry is nice.[(triple14 OR ((triple15) -> rule2))] Harry is smart.[(triple15)] @1: Bob is nice.[(((triple3) -> rule2))] Bob is rough.[(((triple3) -> rule4) OR ((((triple3) -> rule2)) -> rule3))] Harry is rough.[(((triple15) -> rule4))] @2: Bob is green.[(((((triple3) -> rule4)) -> rule5) OR ((((((triple3) -> rule2)) -> rule3)) -> rule5))] Harry is green.[(((((triple15) -> rule4)) -> rule5))] @3: Harry is round.[(((((((triple15) -> rule4)) -> rule5) triple13) -> rule1))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
((((((triple3) -> (rule4 % int3))) -> (rule5 % int2)) triple1) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
((((((((triple3) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule5 % int2)) triple1) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
int4
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
triple4
Charlie is blue.
("Charlie" "is" "blue" "+")
triple5
Charlie is green.
("Charlie" "is" "green" "+")
triple6
((triple8) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((((triple10) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple7
((triple10) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple8
((triple10) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple9
((triple6 triple5) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((((triple8) -> (rule5 % int2)) triple5) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((((((triple10) -> (rule4 % int3))) -> (rule5 % int2)) triple5) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
triple10
Gary is blue.
("Gary" "is" "blue" "+")
triple11
Gary is round.
("Gary" "is" "round" "+")
triple12
Harry is blue.
("Harry" "is" "blue" "+")
triple13
Harry is nice.
("Harry" "is" "nice" "+")
triple14
((triple15) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
triple15
Bob is nice.
("Bob" "is" "nice" "+")
((triple3) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((triple3) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((triple15) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
((((triple15) -> (rule4 % int2))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((((((triple15) -> (rule4 % int3))) -> (rule5 % int2)) triple13) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3