Bob is quiet. Bob is red. Bob is not rough. Bob is round. Charlie is cold. Charlie is quiet. Charlie is round. Fiona is quiet. Fiona is red. Fiona is round. Fiona is not smart. Gary is quiet. Gary is red. Gary is rough. Gary is not white. Quiet things are cold. If Fiona is not round then Fiona is not quiet.
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is not rough.
("Bob" "is" "rough" "-")
Bob is round.
("Bob" "is" "round" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is not smart.
("Fiona" "is" "smart" "-")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is not white.
("Gary" "is" "white" "-")
Quiet things are cold.
((("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
If Fiona is not round then Fiona is not quiet.
((("Fiona" "is" "round" "~")) -> ("Fiona" "is" "quiet" "-"))
Charlie is round.
True
1
proof
[(triple7)]
("Charlie" "is" "round" "+")
triple7
Bob is not red.
False
1
inv-proof
[(triple2)]
("Bob" "is" "red" "-")
triple2
Fiona is cold.
True
2
proof
[(((triple8) -> rule1))]
("Fiona" "is" "cold" "+")
((triple8) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Gary is not cold.
False
2
inv-proof
[(((triple12) -> rule1))]
("Gary" "is" "cold" "-")
((triple12) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Fiona is not white.
Unknown
inv-random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
@0: Bob is not rough.[(triple3)] Bob is quiet.[(triple1)] Bob is red.[(triple2)] Bob is round.[(triple4)] Charlie is cold.[(triple5 OR ((triple6) -> rule1))] Charlie is quiet.[(triple6)] Charlie is round.[(triple7)] Fiona is not smart.[(triple11)] Fiona is quiet.[(triple8)] Fiona is red.[(triple9)] Fiona is round.[(triple10)] Gary is not white.[(triple15)] Gary is quiet.[(triple12)] Gary is red.[(triple13)] Gary is rough.[(triple14)] @1: Bob is cold.[(((triple1) -> rule1))] Fiona is cold.[(((triple8) -> rule1))] Gary is cold.[(((triple12) -> rule1))]
Bob is not rough.
("Bob" "is" "rough" "-")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple4
Charlie is cold.
("Charlie" "is" "cold" "+")
triple5
((triple6) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple6
Charlie is round.
("Charlie" "is" "round" "+")
triple7
Fiona is not smart.
("Fiona" "is" "smart" "-")
triple11
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple8
Fiona is red.
("Fiona" "is" "red" "+")
triple9
Fiona is round.
("Fiona" "is" "round" "+")
triple10
Gary is not white.
("Gary" "is" "white" "-")
triple15
Gary is quiet.
("Gary" "is" "quiet" "+")
triple12
Gary is red.
("Gary" "is" "red" "+")
triple13
Gary is rough.
("Gary" "is" "rough" "+")
triple14
Bob is cold.
("Bob" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple8) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((triple12) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1