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