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