Dave is cold. Dave is green. Dave is kind. Dave is nice. Dave is red. Dave is rough. Dave is smart. Gary is nice. Harry is not green. Harry is nice. Harry is rough. Harry is smart. All smart, kind people are cold. If Harry is not cold then Harry is rough. If someone is nice and not rough then they are red. Nice people are red. Smart people are nice. Rough, red people are nice.
Dave is cold.
("Dave" "is" "cold" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Harry is not green.
("Harry" "is" "green" "-")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All smart, kind people are cold.
((("someone" "is" "smart" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
If Harry is not cold then Harry is rough.
((("Harry" "is" "cold" "~")) -> ("Harry" "is" "rough" "+"))
If someone is nice and not rough then they are red.
((("someone" "is" "nice" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "red" "+"))
Nice people are red.
((("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
Smart people are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
Rough, red people are nice.
((("someone" "is" "rough" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
Gary is nice.
True
1
proof
[(triple8)]
("Gary" "is" "nice" "+")
triple8
Dave is not nice.
False
1
inv-proof
[(triple4 OR ((triple7) -> rule5) OR ((triple6 triple5) -> rule6))]
("Dave" "is" "nice" "-")
triple4
((triple7) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple6 triple5) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Gary is red.
True
2
proof
[(((triple8) -> rule4))]
("Gary" "is" "red" "+")
((triple8) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is not red.
False
2
inv-proof
[(((triple8) -> rule4))]
("Gary" "is" "red" "-")
((triple8) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is not cold.
Unknown
inv-rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "cold" "-")
Harry is cold.
Unknown
rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "cold" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Dave is cold.[(triple1 OR ((triple7 triple3) -> rule1))] Dave is green.[(triple2)] Dave is kind.[(triple3)] Dave is nice.[(triple4 OR ((triple7) -> rule5) OR ((triple6 triple5) -> rule6))] Dave is red.[(triple5 OR ((triple4) -> rule4) OR ((((triple7) -> rule5)) -> rule4))] Dave is rough.[(triple6)] Dave is smart.[(triple7)] Gary is nice.[(triple8)] Harry is nice.[(triple10 OR ((triple12) -> rule5))] Harry is not green.[(triple9)] Harry is rough.[(triple11)] Harry is smart.[(triple12)] @1: Gary is red.[(((triple8) -> rule4))] Harry is red.[(((triple10) -> rule4) OR ((((triple12) -> rule5)) -> rule4))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
((triple7 triple3) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
triple4
((triple7) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple6 triple5) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple5
((triple4) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((((triple7) -> (rule5 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
triple6
Dave is smart.
("Dave" "is" "smart" "+")
triple7
Gary is nice.
("Gary" "is" "nice" "+")
triple8
Harry is nice.
("Harry" "is" "nice" "+")
triple10
((triple12) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not green.
("Harry" "is" "green" "-")
triple9
Harry is rough.
("Harry" "is" "rough" "+")
triple11
Harry is smart.
("Harry" "is" "smart" "+")
triple12
Gary is red.
("Gary" "is" "red" "+")
((triple8) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple10) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((triple12) -> (rule5 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2