Fiona is big. Fiona is cold. Fiona is nice. Fiona is round. Gary is cold. Gary is kind. Gary is nice. Gary is not round. Harry is blue. Harry is cold. Harry is kind. Harry is round. If Gary is smart then Gary is kind. If something is kind then it is nice. If Gary is blue then Gary is big. If something is round and not kind then it is cold. If Gary is smart and Gary is cold then Gary is nice. If Gary is not round and Gary is not kind then Gary is nice. If something is smart and big then it is not blue. All nice, blue things are big.
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is not round.
("Gary" "is" "round" "-")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is round.
("Harry" "is" "round" "+")
If Gary is smart then Gary is kind.
((("Gary" "is" "smart" "+")) -> ("Gary" "is" "kind" "+"))
If something is kind then it is nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
If Gary is blue then Gary is big.
((("Gary" "is" "blue" "+")) -> ("Gary" "is" "big" "+"))
If something is round and not kind then it is cold.
((("something" "is" "round" "+") ("something" "is" "kind" "~")) -> ("something" "is" "cold" "+"))
If Gary is smart and Gary is cold then Gary is nice.
((("Gary" "is" "smart" "+") ("Gary" "is" "cold" "+")) -> ("Gary" "is" "nice" "+"))
If Gary is not round and Gary is not kind then Gary is nice.
((("Gary" "is" "round" "~") ("Gary" "is" "kind" "~")) -> ("Gary" "is" "nice" "+"))
If something is smart and big then it is not blue.
((("something" "is" "smart" "+") ("something" "is" "big" "+")) -> ("something" "is" "blue" "-"))
All nice, blue things are big.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
Harry is round.
True
1
proof
[(triple12)]
("Harry" "is" "round" "+")
triple12
Gary is not cold.
False
1
inv-proof
[(triple5)]
("Gary" "is" "cold" "-")
triple5
Harry is nice.
True
2
proof
[(((triple11) -> rule2))]
("Harry" "is" "nice" "+")
((triple11) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not nice.
False
2
inv-proof
[(((triple11) -> rule2))]
("Harry" "is" "nice" "-")
((triple11) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
True
4
proof
[(((((triple11) -> rule2) triple9) -> rule8))]
("Harry" "is" "big" "+")
((((triple11) -> (rule2 % int2)) triple9) -> (rule8 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is not big.
False
4
inv-proof
[(((((triple11) -> rule2) triple9) -> rule8))]
("Harry" "is" "big" "-")
((((triple11) -> (rule2 % int2)) triple9) -> (rule8 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Gary is not big.
Unknown
inv-rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "big" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
@0: Fiona is big.[(triple1)] Fiona is cold.[(triple2)] Fiona is nice.[(triple3)] Fiona is round.[(triple4)] Gary is cold.[(triple5)] Gary is kind.[(triple6)] Gary is nice.[(triple7 OR ((triple6) -> rule2))] Gary is not round.[(triple8)] Harry is blue.[(triple9)] Harry is cold.[(triple10)] Harry is kind.[(triple11)] Harry is round.[(triple12)] @1: Harry is nice.[(((triple11) -> rule2))] @2: Harry is big.[(((((triple11) -> rule2) triple9) -> rule8))]
Fiona is big.
("Fiona" "is" "big" "+")
triple1
Fiona is cold.
("Fiona" "is" "cold" "+")
triple2
Fiona is nice.
("Fiona" "is" "nice" "+")
triple3
Fiona is round.
("Fiona" "is" "round" "+")
triple4
Gary is cold.
("Gary" "is" "cold" "+")
triple5
Gary is kind.
("Gary" "is" "kind" "+")
triple6
Gary is nice.
("Gary" "is" "nice" "+")
triple7
((triple6) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is not round.
("Gary" "is" "round" "-")
triple8
Harry is blue.
("Harry" "is" "blue" "+")
triple9
Harry is cold.
("Harry" "is" "cold" "+")
triple10
Harry is kind.
("Harry" "is" "kind" "+")
triple11
Harry is round.
("Harry" "is" "round" "+")
triple12
Harry is nice.
("Harry" "is" "nice" "+")
((triple11) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((((triple11) -> (rule2 % int2)) triple9) -> (rule8 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2