Bob is cold. Bob is green. Bob is rough. Bob is smart. Charlie is furry. Charlie is green. Charlie is not quiet. Charlie is rough. Charlie is smart. Charlie is white. Fiona is green. Fiona is smart. Gary is furry. Gary is quiet. Gary is rough. Gary is white. If someone is rough and not white then they are quiet. If Fiona is cold then Fiona is quiet. All smart people are cold.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is white.
("Gary" "is" "white" "+")
If someone is rough and not white then they are quiet.
((("someone" "is" "rough" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "quiet" "+"))
If Fiona is cold then Fiona is quiet.
((("Fiona" "is" "cold" "+")) -> ("Fiona" "is" "quiet" "+"))
All smart people are cold.
((("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
Charlie is green.
True
1
proof
[(triple6)]
("Charlie" "is" "green" "+")
triple6
Bob is not smart.
False
1
inv-proof
[(triple4)]
("Bob" "is" "smart" "-")
triple4
Fiona is cold.
True
2
proof
[(((triple12) -> rule3))]
("Fiona" "is" "cold" "+")
((triple12) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Charlie is not cold.
False
2
inv-proof
[(((triple9) -> rule3))]
("Charlie" "is" "cold" "-")
((triple9) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Fiona is quiet.
True
3
proof
[(((((triple12) -> rule3)) -> rule2))]
("Fiona" "is" "quiet" "+")
((((triple12) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is not quiet.
False
3
inv-proof
[(((((triple12) -> rule3)) -> rule2))]
("Fiona" "is" "quiet" "-")
((((triple12) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "quiet" "-")
Gary is cold.
Unknown
rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "cold" "+")
Fiona is not furry.
Unknown
inv-random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
Fiona is not rough.
Unknown
inv-random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
@0: Bob is cold.[(triple1 OR ((triple4) -> rule3))] Bob is green.[(triple2)] Bob is rough.[(triple3)] Bob is smart.[(triple4)] Charlie is furry.[(triple5)] Charlie is green.[(triple6)] Charlie is not quiet.[(triple7)] Charlie is rough.[(triple8)] Charlie is smart.[(triple9)] Charlie is white.[(triple10)] Fiona is green.[(triple11)] Fiona is smart.[(triple12)] Gary is furry.[(triple13)] Gary is quiet.[(triple14)] Gary is rough.[(triple15)] Gary is white.[(triple16)] @1: Charlie is cold.[(((triple9) -> rule3))] Fiona is cold.[(((triple12) -> rule3))] @2: Fiona is quiet.[(((((triple12) -> rule3)) -> rule2))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
((triple4) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is rough.
("Bob" "is" "rough" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
triple4
Charlie is furry.
("Charlie" "is" "furry" "+")
triple5
Charlie is green.
("Charlie" "is" "green" "+")
triple6
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
triple7
Charlie is rough.
("Charlie" "is" "rough" "+")
triple8
Charlie is smart.
("Charlie" "is" "smart" "+")
triple9
Charlie is white.
("Charlie" "is" "white" "+")
triple10
Fiona is green.
("Fiona" "is" "green" "+")
triple11
Fiona is smart.
("Fiona" "is" "smart" "+")
triple12
Gary is furry.
("Gary" "is" "furry" "+")
triple13
Gary is quiet.
("Gary" "is" "quiet" "+")
triple14
Gary is rough.
("Gary" "is" "rough" "+")
triple15
Gary is white.
("Gary" "is" "white" "+")
triple16
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple9) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple12) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((triple12) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2