Dave is nice. Dave is quiet. Dave is smart. Fiona is big. Gary is big. Gary is cold. Gary is green. Gary is nice. Gary is round. Gary is smart. Harry is big. Harry is round. If someone is cold and smart then they are green. Nice people are cold.
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is round.
("Harry" "is" "round" "+")
If someone is cold and smart then they are green.
((("someone" "is" "cold" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
Nice people are cold.
((("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
Gary is nice.
True
1
proof
[(triple8)]
("Gary" "is" "nice" "+")
triple8
Dave is not quiet.
False
1
inv-proof
[(triple2)]
("Dave" "is" "quiet" "-")
triple2
Dave is cold.
True
2
proof
[(((triple1) -> rule2))]
("Dave" "is" "cold" "+")
((triple1) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is not cold.
False
2
inv-proof
[(((triple1) -> rule2))]
("Dave" "is" "cold" "-")
((triple1) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is green.
True
4
proof
[(((((triple1) -> rule2) triple3) -> rule1))]
("Dave" "is" "green" "+")
((((triple1) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is not green.
False
4
inv-proof
[(((((triple1) -> rule2) triple3) -> rule1))]
("Dave" "is" "green" "-")
((((triple1) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Fiona is not cold.
Unknown
inv-rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "cold" "-")
Fiona is green.
Unknown
rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "green" "+")
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "cold" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
@0: Dave is nice.[(triple1)] Dave is quiet.[(triple2)] Dave is smart.[(triple3)] Fiona is big.[(triple4)] Gary is big.[(triple5)] Gary is cold.[(triple6 OR ((triple8) -> rule2))] Gary is green.[(triple7 OR ((triple6 triple10) -> rule1) OR ((((triple8) -> rule2) triple10) -> rule1))] Gary is nice.[(triple8)] Gary is round.[(triple9)] Gary is smart.[(triple10)] Harry is big.[(triple11)] Harry is round.[(triple12)] @1: Dave is cold.[(((triple1) -> rule2))] @2: Dave is green.[(((((triple1) -> rule2) triple3) -> rule1))]
Dave is nice.
("Dave" "is" "nice" "+")
triple1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
triple3
Fiona is big.
("Fiona" "is" "big" "+")
triple4
Gary is big.
("Gary" "is" "big" "+")
triple5
Gary is cold.
("Gary" "is" "cold" "+")
triple6
((triple8) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
triple7
((triple6 triple10) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple8) -> (rule2 % int2)) triple10) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
triple8
Gary is round.
("Gary" "is" "round" "+")
triple9
Gary is smart.
("Gary" "is" "smart" "+")
triple10
Harry is big.
("Harry" "is" "big" "+")
triple11
Harry is round.
("Harry" "is" "round" "+")
triple12
Dave is cold.
("Dave" "is" "cold" "+")
((triple1) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((((triple1) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2