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