Charlie is cold. Charlie is quiet. Charlie is red. Charlie is rough. Charlie is white. Charlie is young. Dave is not green. Dave is not quiet. Dave is rough. Dave is not young. Harry is cold. Harry is green. Harry is quiet. Harry is rough. Harry is white. Harry is young. Red people are cold. If someone is green and not red then they are cold. Green people are cold. All red people are not green. Green, cold people are young. If someone is red and not rough then they are quiet. Red people are quiet. If Charlie is red and Charlie is rough then Charlie is cold.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is not green.
("Dave" "is" "green" "-")
Dave is not quiet.
("Dave" "is" "quiet" "-")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is not young.
("Dave" "is" "young" "-")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
Red people are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
If someone is green and not red then they are cold.
((("someone" "is" "green" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "cold" "+"))
Green people are cold.
((("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
All red people are not green.
((("someone" "is" "red" "+")) -> ("someone" "is" "green" "-"))
Green, cold people are young.
((("someone" "is" "green" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
If someone is red and not rough then they are quiet.
((("someone" "is" "red" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "quiet" "+"))
Red people are quiet.
((("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
If Charlie is red and Charlie is rough then Charlie is cold.
((("Charlie" "is" "red" "+") ("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "cold" "+"))
Harry is green.
True
1
proof
[(triple12)]
("Harry" "is" "green" "+")
triple12
Dave is young.
False
1
inv-proof
[(triple10)]
("Dave" "is" "young" "+")
triple10
Charlie is not green.
True
2
proof
[(((triple3) -> rule4))]
("Charlie" "is" "green" "-")
((triple3) -> (rule4 % int1))
Charlie is not green.
("Charlie" "is" "green" "-")
int1
Charlie is green.
False
2
inv-proof
[(((triple3) -> rule4))]
("Charlie" "is" "green" "+")
((triple3) -> (rule4 % int1))
Charlie is not green.
("Charlie" "is" "green" "-")
int1
Dave is not cold.
Unknown
inv-rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "cold" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
@0: Charlie is cold.[(triple1 OR ((triple3) -> rule1) OR ((triple3 triple4) -> rule8))] Charlie is quiet.[(triple2 OR ((triple3) -> rule7))] Charlie is red.[(triple3)] Charlie is rough.[(triple4)] Charlie is white.[(triple5)] Charlie is young.[(triple6)] Dave is not green.[(triple7)] Dave is not quiet.[(triple8)] Dave is not young.[(triple10)] Dave is rough.[(triple9)] Harry is cold.[(triple11 OR ((triple12) -> rule3))] Harry is green.[(triple12)] Harry is quiet.[(triple13)] Harry is rough.[(triple14)] Harry is white.[(triple15)] Harry is young.[(triple16 OR ((triple12 triple11) -> rule5) OR ((triple12 ((triple12) -> rule3)) -> rule5))] @1: Charlie is not green.[(((triple3) -> rule4))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
((triple3) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((triple3 triple4) -> (rule8 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
((triple3) -> (rule7 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
triple3
Charlie is rough.
("Charlie" "is" "rough" "+")
triple4
Charlie is white.
("Charlie" "is" "white" "+")
triple5
Charlie is young.
("Charlie" "is" "young" "+")
triple6
Dave is not green.
("Dave" "is" "green" "-")
triple7
Dave is not quiet.
("Dave" "is" "quiet" "-")
triple8
Dave is not young.
("Dave" "is" "young" "-")
triple10
Dave is rough.
("Dave" "is" "rough" "+")
triple9
Harry is cold.
("Harry" "is" "cold" "+")
triple11
((triple12) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple12
Harry is quiet.
("Harry" "is" "quiet" "+")
triple13
Harry is rough.
("Harry" "is" "rough" "+")
triple14
Harry is white.
("Harry" "is" "white" "+")
triple15
Harry is young.
("Harry" "is" "young" "+")
triple16
((triple12 triple11) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple12 ((triple12) -> (rule3 % int2))) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Charlie is not green.
("Charlie" "is" "green" "-")
((triple3) -> (rule4 % int1))
Charlie is not green.
("Charlie" "is" "green" "-")
int1