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