Bob is cold. Bob is green. Bob is quiet. Bob is round. Erin is smart. Fiona is cold. Fiona is kind. Fiona is quiet. Fiona is round. Fiona is smart. All cold people are quiet. Cold, big people are smart. All big people are green. If someone is round then they are quiet. If Bob is round and Bob is cold then Bob is quiet. All green people are smart.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
All cold people are quiet.
((("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
Cold, big people are smart.
((("someone" "is" "cold" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
All big people are green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
If someone is round then they are quiet.
((("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
If Bob is round and Bob is cold then Bob is quiet.
((("Bob" "is" "round" "+") ("Bob" "is" "cold" "+")) -> ("Bob" "is" "quiet" "+"))
All green people are smart.
((("someone" "is" "green" "+")) -> ("someone" "is" "smart" "+"))
Fiona is smart.
True
1
proof
[(triple10)]
("Fiona" "is" "smart" "+")
triple10
Fiona is not round.
False
1
inv-proof
[(triple9)]
("Fiona" "is" "round" "-")
triple9
Bob is smart.
True
2
proof
[(((triple2) -> rule6))]
("Bob" "is" "smart" "+")
((triple2) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is not smart.
False
2
inv-proof
[(((triple2) -> rule6))]
("Bob" "is" "smart" "-")
((triple2) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Erin is not green.
Unknown
inv-rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "green" "-")
Fiona is green.
Unknown
rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "green" "+")
Erin is not kind.
Unknown
inv-random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
@0: Bob is cold.[(triple1)] Bob is green.[(triple2)] Bob is quiet.[(triple3 OR ((triple1) -> rule1) OR ((triple4) -> rule4) OR ((triple4 triple1) -> rule5))] Bob is round.[(triple4)] Erin is smart.[(triple5)] Fiona is cold.[(triple6)] Fiona is kind.[(triple7)] Fiona is quiet.[(triple8 OR ((triple6) -> rule1) OR ((triple9) -> rule4))] Fiona is round.[(triple9)] Fiona is smart.[(triple10)] @1: Bob is smart.[(((triple2) -> rule6))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
((triple1) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple4) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple4 triple1) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple4
Erin is smart.
("Erin" "is" "smart" "+")
triple5
Fiona is cold.
("Fiona" "is" "cold" "+")
triple6
Fiona is kind.
("Fiona" "is" "kind" "+")
triple7
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple8
((triple6) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
((triple9) -> (rule4 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
triple9
Fiona is smart.
("Fiona" "is" "smart" "+")
triple10
Bob is smart.
("Bob" "is" "smart" "+")
((triple2) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1