Charlie is red. Charlie is smart. Dave is blue. Dave is nice. Dave is quiet. Gary is blue. Gary is green. Gary is nice. Gary is quiet. Gary is rough. Harry is blue. Harry is quiet. Harry is red. Harry is rough. Harry is smart. Red, quiet things are smart. All nice things are green. Green things are red.
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Red, quiet things are smart.
((("something" "is" "red" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
All nice things are green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
Green things are red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
Dave is blue.
True
1
proof
[(triple3)]
("Dave" "is" "blue" "+")
triple3
Charlie is not smart.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "smart" "-")
triple2
Gary is red.
True
2
proof
[(((triple7) -> rule3) OR ((((triple8) -> rule2)) -> rule3))]
("Gary" "is" "red" "+")
((triple7) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Dave is not green.
False
2
inv-proof
[(((triple4) -> rule2))]
("Dave" "is" "green" "-")
((triple4) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
True
3
proof
[(((((triple4) -> rule2)) -> rule3))]
("Dave" "is" "red" "+")
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Gary is not smart.
False
4
inv-proof
[(((((triple7) -> rule3) triple9) -> rule1) OR ((((((triple8) -> rule2)) -> rule3) triple9) -> rule1))]
("Gary" "is" "smart" "-")
((((triple7) -> (rule3 % int2)) triple9) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((((triple8) -> (rule2 % int3))) -> (rule3 % int2)) triple9) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Dave is smart.
True
5
proof
[(((((((triple4) -> rule2)) -> rule3) triple5) -> rule1))]
("Dave" "is" "smart" "+")
((((((triple4) -> (rule2 % int3))) -> (rule3 % int2)) triple5) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is not smart.
False
5
inv-proof
[(((((((triple4) -> rule2)) -> rule3) triple5) -> rule1))]
("Dave" "is" "smart" "-")
((((((triple4) -> (rule2 % int3))) -> (rule3 % int2)) triple5) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Charlie is not green.
Unknown
inv-rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "green" "-")
Harry is green.
Unknown
rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "green" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
Charlie is not rough.
Unknown
inv-random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
@0: Charlie is red.[(triple1)] Charlie is smart.[(triple2)] Dave is blue.[(triple3)] Dave is nice.[(triple4)] Dave is quiet.[(triple5)] Gary is blue.[(triple6)] Gary is green.[(triple7 OR ((triple8) -> rule2))] Gary is nice.[(triple8)] Gary is quiet.[(triple9)] Gary is rough.[(triple10)] Harry is blue.[(triple11)] Harry is quiet.[(triple12)] Harry is red.[(triple13)] Harry is rough.[(triple14)] Harry is smart.[(triple15 OR ((triple13 triple12) -> rule1))] @1: Dave is green.[(((triple4) -> rule2))] Gary is red.[(((triple7) -> rule3) OR ((((triple8) -> rule2)) -> rule3))] @2: Dave is red.[(((((triple4) -> rule2)) -> rule3))] Gary is smart.[(((((triple7) -> rule3) triple9) -> rule1) OR ((((((triple8) -> rule2)) -> rule3) triple9) -> rule1))] @3: Dave is smart.[(((((((triple4) -> rule2)) -> rule3) triple5) -> rule1))]
Charlie is red.
("Charlie" "is" "red" "+")
triple1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple2
Dave is blue.
("Dave" "is" "blue" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
triple4
Dave is quiet.
("Dave" "is" "quiet" "+")
triple5
Gary is blue.
("Gary" "is" "blue" "+")
triple6
Gary is green.
("Gary" "is" "green" "+")
triple7
((triple8) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
triple8
Gary is quiet.
("Gary" "is" "quiet" "+")
triple9
Gary is rough.
("Gary" "is" "rough" "+")
triple10
Harry is blue.
("Harry" "is" "blue" "+")
triple11
Harry is quiet.
("Harry" "is" "quiet" "+")
triple12
Harry is red.
("Harry" "is" "red" "+")
triple13
Harry is rough.
("Harry" "is" "rough" "+")
triple14
Harry is smart.
("Harry" "is" "smart" "+")
triple15
((triple13 triple12) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((triple4) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple7) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((((triple7) -> (rule3 % int2)) triple9) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((((triple8) -> (rule2 % int3))) -> (rule3 % int2)) triple9) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
((((((triple4) -> (rule2 % int3))) -> (rule3 % int2)) triple5) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3