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