Charlie is green. Charlie is kind. Charlie is quiet. Dave is big. Dave is cold. Dave is kind. Dave is quiet. Dave is red. Dave is young. Harry is cold. Harry is red. Harry is young. All green, kind things are young. All cold, green things are kind. If Charlie is quiet then Charlie is cold.
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is young.
("Harry" "is" "young" "+")
All green, kind things are young.
((("something" "is" "green" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
All cold, green things are kind.
((("something" "is" "cold" "+") ("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
If Charlie is quiet then Charlie is cold.
((("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "cold" "+"))
Charlie is kind.
True
1
proof
[(triple2 OR ((((triple3) -> rule3) triple1) -> rule2))]
("Charlie" "is" "kind" "+")
triple2
((((triple3) -> (rule3 % int2)) triple1) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Dave is not quiet.
False
1
inv-proof
[(triple7)]
("Dave" "is" "quiet" "-")
triple7
Charlie is young.
True
3
proof
[(((triple1 triple2) -> rule1) OR ((triple1 ((((triple3) -> rule3) triple1) -> rule2)) -> rule1))]
("Charlie" "is" "young" "+")
((triple1 triple2) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple1 ((((triple3) -> (rule3 % int3)) triple1) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is not young.
False
3
inv-proof
[(((triple1 triple2) -> rule1) OR ((triple1 ((((triple3) -> rule3) triple1) -> rule2)) -> rule1))]
("Charlie" "is" "young" "-")
((triple1 triple2) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple1 ((((triple3) -> (rule3 % int3)) triple1) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Harry is not kind.
Unknown
inv-rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "kind" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
@0: Charlie is green.[(triple1)] Charlie is kind.[(triple2 OR ((((triple3) -> rule3) triple1) -> rule2))] Charlie is quiet.[(triple3)] Dave is big.[(triple4)] Dave is cold.[(triple5)] Dave is kind.[(triple6)] Dave is quiet.[(triple7)] Dave is red.[(triple8)] Dave is young.[(triple9)] Harry is cold.[(triple10)] Harry is red.[(triple11)] Harry is young.[(triple12)] @1: Charlie is cold.[(((triple3) -> rule3))] Charlie is young.[(((triple1 triple2) -> rule1) OR ((triple1 ((((triple3) -> rule3) triple1) -> rule2)) -> rule1))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
((((triple3) -> (rule3 % int2)) triple1) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Dave is big.
("Dave" "is" "big" "+")
triple4
Dave is cold.
("Dave" "is" "cold" "+")
triple5
Dave is kind.
("Dave" "is" "kind" "+")
triple6
Dave is quiet.
("Dave" "is" "quiet" "+")
triple7
Dave is red.
("Dave" "is" "red" "+")
triple8
Dave is young.
("Dave" "is" "young" "+")
triple9
Harry is cold.
("Harry" "is" "cold" "+")
triple10
Harry is red.
("Harry" "is" "red" "+")
triple11
Harry is young.
("Harry" "is" "young" "+")
triple12
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple3) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((triple1 triple2) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple1 ((((triple3) -> (rule3 % int3)) triple1) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3