Bob is blue. Dave is quiet. Dave is red. Dave is smart. Gary is blue. Gary is green. Gary is quiet. Gary is smart. Harry is green. Harry is quiet. Harry is red. If Bob is quiet and Bob is kind then Bob is smart. All kind things are green. Quiet, red things are kind. If something is green then it is quiet. If Bob is blue then Bob is kind. If Harry is young then Harry is kind. If something is blue then it is young. If something is smart and green then it is blue. All kind, smart things are red.
Bob is blue.
("Bob" "is" "blue" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
If Bob is quiet and Bob is kind then Bob is smart.
((("Bob" "is" "quiet" "+") ("Bob" "is" "kind" "+")) -> ("Bob" "is" "smart" "+"))
All kind things are green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
Quiet, red things are kind.
((("something" "is" "quiet" "+") ("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
If something is green then it is quiet.
((("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
If Bob is blue then Bob is kind.
((("Bob" "is" "blue" "+")) -> ("Bob" "is" "kind" "+"))
If Harry is young then Harry is kind.
((("Harry" "is" "young" "+")) -> ("Harry" "is" "kind" "+"))
If something is blue then it is young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
If something is smart and green then it is blue.
((("something" "is" "smart" "+") ("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
All kind, smart things are red.
((("something" "is" "kind" "+") ("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
Dave is smart.
True
1
proof
[(triple4)]
("Dave" "is" "smart" "+")
triple4
Gary is not smart.
False
1
inv-proof
[(triple8)]
("Gary" "is" "smart" "-")
triple8
Bob is kind.
True
2
proof
[(((triple1) -> rule5))]
("Bob" "is" "kind" "+")
((triple1) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Harry is not kind.
False
3
inv-proof
[(((triple10 triple11) -> rule3) OR ((((triple9) -> rule4) triple11) -> rule3))]
("Harry" "is" "kind" "-")
((triple10 triple11) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((((triple9) -> (rule4 % int2)) triple11) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Bob is green.
True
3
proof
[(((((triple1) -> rule5)) -> rule2))]
("Bob" "is" "green" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Dave is not green.
False
4
inv-proof
[(((((triple2 triple3) -> rule3)) -> rule2))]
("Dave" "is" "green" "-")
((((triple2 triple3) -> (rule3 % int2))) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is blue.
True
6
proof
[(((triple4 ((((triple2 triple3) -> rule3)) -> rule2)) -> rule8))]
("Dave" "is" "blue" "+")
((triple4 ((((triple2 triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is not blue.
False
6
inv-proof
[(((triple4 ((((triple2 triple3) -> rule3)) -> rule2)) -> rule8))]
("Dave" "is" "blue" "-")
((triple4 ((((triple2 triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Bob is smart.
True
7
proof
[(((((((((triple1) -> rule5)) -> rule2)) -> rule4) ((triple1) -> rule5)) -> rule1))]
("Bob" "is" "smart" "+")
((((((((triple1) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule4 % int2)) ((triple1) -> (rule5 % int4))) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4
Dave is not young.
False
7
inv-proof
[(((((triple4 ((((triple2 triple3) -> rule3)) -> rule2)) -> rule8)) -> rule7))]
("Dave" "is" "young" "-")
((((triple4 ((((triple2 triple3) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Bob is red.
True
10
proof
[(((((triple1) -> rule5) ((((((((triple1) -> rule5)) -> rule2)) -> rule4) ((triple1) -> rule5)) -> rule1)) -> rule9))]
("Bob" "is" "red" "+")
((((triple1) -> (rule5 % int5)) ((((((((triple1) -> (rule5 % int5))) -> (rule2 % int4))) -> (rule4 % int3)) ((triple1) -> (rule5 % int5))) -> (rule1 % int2))) -> (rule9 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Bob is kind.
("Bob" "is" "kind" "+")
int5
Bob is not red.
False
10
inv-proof
[(((((triple1) -> rule5) ((((((((triple1) -> rule5)) -> rule2)) -> rule4) ((triple1) -> rule5)) -> rule1)) -> rule9))]
("Bob" "is" "red" "-")
((((triple1) -> (rule5 % int5)) ((((((((triple1) -> (rule5 % int5))) -> (rule2 % int4))) -> (rule4 % int3)) ((triple1) -> (rule5 % int5))) -> (rule1 % int2))) -> (rule9 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Bob is kind.
("Bob" "is" "kind" "+")
int5
Harry is not blue.
Unknown
inv-rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Harry" "is" "blue" "-")
Harry is young.
Unknown
rconc
[@2: Harry is young.[CWA. Example of deepest failure = (rule7 <- rule8 <- FAIL)]]
("Harry" "is" "young" "+")
Gary is not kind.
Unknown
inv-rconc
[@2: Gary is kind.[CWA. Example of deepest failure = (rule3 <- rule9 <- FAIL)]]
("Gary" "is" "kind" "-")
Gary is red.
Unknown
rconc
[@2: Gary is red.[CWA. Example of deepest failure = (rule9 <- rule3 <- FAIL)]]
("Gary" "is" "red" "+")
@0: Bob is blue.[(triple1)] Dave is quiet.[(triple2)] Dave is red.[(triple3)] Dave is smart.[(triple4)] Gary is blue.[(triple5 OR ((triple8 triple6) -> rule8))] Gary is green.[(triple6)] Gary is quiet.[(triple7 OR ((triple6) -> rule4))] Gary is smart.[(triple8)] Harry is green.[(triple9 OR ((((triple10 triple11) -> rule3)) -> rule2))] Harry is quiet.[(triple10 OR ((triple9) -> rule4))] Harry is red.[(triple11)] @1: Bob is kind.[(((triple1) -> rule5))] Bob is young.[(((triple1) -> rule7))] Dave is kind.[(((triple2 triple3) -> rule3))] Gary is young.[(((triple5) -> rule7) OR ((((triple8 triple6) -> rule8)) -> rule7))] Harry is kind.[(((triple10 triple11) -> rule3) OR ((((triple9) -> rule4) triple11) -> rule3))] @2: Bob is green.[(((((triple1) -> rule5)) -> rule2))] Dave is green.[(((((triple2 triple3) -> rule3)) -> rule2))] @3: Bob is quiet.[(((((((triple1) -> rule5)) -> rule2)) -> rule4))] Dave is blue.[(((triple4 ((((triple2 triple3) -> rule3)) -> rule2)) -> rule8))] @4: Bob is smart.[(((((((((triple1) -> rule5)) -> rule2)) -> rule4) ((triple1) -> rule5)) -> rule1))] Dave is young.[(((((triple4 ((((triple2 triple3) -> rule3)) -> rule2)) -> rule8)) -> rule7))] @5: Bob is red.[(((((triple1) -> rule5) ((((((((triple1) -> rule5)) -> rule2)) -> rule4) ((triple1) -> rule5)) -> rule1)) -> rule9))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
Dave is red.
("Dave" "is" "red" "+")
triple3
Dave is smart.
("Dave" "is" "smart" "+")
triple4
Gary is blue.
("Gary" "is" "blue" "+")
triple5
((triple8 triple6) -> (rule8 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
triple6
Gary is quiet.
("Gary" "is" "quiet" "+")
triple7
((triple6) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple8
Harry is green.
("Harry" "is" "green" "+")
triple9
((((triple10 triple11) -> (rule3 % int2))) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
((triple9) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple11
Bob is kind.
("Bob" "is" "kind" "+")
((triple1) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((triple1) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((triple2 triple3) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple5) -> (rule7 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((((triple8 triple6) -> (rule8 % int2))) -> (rule7 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((triple10 triple11) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((((triple9) -> (rule4 % int2)) triple11) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((((triple2 triple3) -> (rule3 % int2))) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
((triple4 ((((triple2 triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
((((((((triple1) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule4 % int2)) ((triple1) -> (rule5 % int4))) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4
Dave is young.
("Dave" "is" "young" "+")
((((triple4 ((((triple2 triple3) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Bob is red.
("Bob" "is" "red" "+")
((((triple1) -> (rule5 % int5)) ((((((((triple1) -> (rule5 % int5))) -> (rule2 % int4))) -> (rule4 % int3)) ((triple1) -> (rule5 % int5))) -> (rule1 % int2))) -> (rule9 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Bob is kind.
("Bob" "is" "kind" "+")
int5