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