Bob is green. Bob is nice. Bob is quiet. Bob is round. Bob is white. Charlie is cold. Charlie is green. Charlie is nice. Charlie is white. Fiona is big. If something is nice then it is quiet. Round things are nice. All cold things are quiet. Green things are big. If something is quiet and cold then it is white. Big things are round. If something is white then it is quiet. If something is nice and cold then it is round.
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Fiona is big.
("Fiona" "is" "big" "+")
If something is nice then it is quiet.
((("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
Round things are nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
All cold things are quiet.
((("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
Green things are big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
If something is quiet and cold then it is white.
((("something" "is" "quiet" "+") ("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
Big things are round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
If something is white then it is quiet.
((("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
If something is nice and cold then it is round.
((("something" "is" "nice" "+") ("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
Bob is white.
True
1
proof
[(triple5)]
("Bob" "is" "white" "+")
triple5
Bob is not green.
False
1
inv-proof
[(triple1)]
("Bob" "is" "green" "-")
triple1
Charlie is quiet.
True
2
proof
[(((triple6) -> rule3) OR ((triple8) -> rule1) OR ((triple9) -> rule7) OR ((((((((triple7) -> rule4)) -> rule6)) -> rule2)) -> rule1))]
("Charlie" "is" "quiet" "+")
((triple6) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((triple8) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((triple9) -> (rule7 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((((((((triple7) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
Charlie is not big.
False
2
inv-proof
[(((triple7) -> rule4))]
("Charlie" "is" "big" "-")
((triple7) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Fiona is nice.
True
3
proof
[(((((triple10) -> rule6)) -> rule2))]
("Fiona" "is" "nice" "+")
((((triple10) -> (rule6 % int2))) -> (rule2 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is not nice.
False
3
inv-proof
[(((((triple10) -> rule6)) -> rule2))]
("Fiona" "is" "nice" "-")
((((triple10) -> (rule6 % int2))) -> (rule2 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is quiet.
True
4
proof
[(((((((triple10) -> rule6)) -> rule2)) -> rule1))]
("Fiona" "is" "quiet" "+")
((((((triple10) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is not quiet.
False
4
inv-proof
[(((((((triple10) -> rule6)) -> rule2)) -> rule1))]
("Fiona" "is" "quiet" "-")
((((((triple10) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is not white.
Unknown
inv-rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "white" "-")
Fiona is green.
Unknown
random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
@0: Bob is green.[(triple1)] Bob is nice.[(triple2 OR ((triple4) -> rule2) OR ((((((triple1) -> rule4)) -> rule6)) -> rule2))] Bob is quiet.[(triple3 OR ((triple2) -> rule1) OR ((triple5) -> rule7) OR ((((triple4) -> rule2)) -> rule1) OR ((((((((triple1) -> rule4)) -> rule6)) -> rule2)) -> rule1))] Bob is round.[(triple4 OR ((((triple1) -> rule4)) -> rule6))] Bob is white.[(triple5)] Charlie is cold.[(triple6)] Charlie is green.[(triple7)] Charlie is nice.[(triple8 OR ((((((triple7) -> rule4)) -> rule6)) -> rule2))] Charlie is white.[(triple9 OR ((((triple6) -> rule3) triple6) -> rule5) OR ((((triple8) -> rule1) triple6) -> rule5) OR ((((((((((triple7) -> rule4)) -> rule6)) -> rule2)) -> rule1) triple6) -> rule5))] Fiona is big.[(triple10)] @1: Bob is big.[(((triple1) -> rule4))] Charlie is big.[(((triple7) -> rule4))] Charlie is quiet.[(((triple6) -> rule3) OR ((triple8) -> rule1) OR ((triple9) -> rule7) OR ((((((((triple7) -> rule4)) -> rule6)) -> rule2)) -> rule1))] Charlie is round.[(((triple8 triple6) -> rule8) OR ((((triple7) -> rule4)) -> rule6))] Fiona is round.[(((triple10) -> rule6))] @2: Fiona is nice.[(((((triple10) -> rule6)) -> rule2))] @3: Fiona is quiet.[(((((((triple10) -> rule6)) -> rule2)) -> rule1))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
((triple4) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
((triple2) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple5) -> (rule7 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((((((triple1) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
Bob is round.
("Bob" "is" "round" "+")
triple4
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
triple5
Charlie is cold.
("Charlie" "is" "cold" "+")
triple6
Charlie is green.
("Charlie" "is" "green" "+")
triple7
Charlie is nice.
("Charlie" "is" "nice" "+")
triple8
((((((triple7) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
triple9
((((triple6) -> (rule3 % int2)) triple6) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple8) -> (rule1 % int2)) triple6) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((((((((triple7) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule1 % int2)) triple6) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
Charlie is big.
("Charlie" "is" "big" "+")
int5
Fiona is big.
("Fiona" "is" "big" "+")
triple10
Bob is big.
("Bob" "is" "big" "+")
((triple1) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((triple7) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple6) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((triple8) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((triple9) -> (rule7 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((((((((triple7) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
Charlie is round.
("Charlie" "is" "round" "+")
((triple8 triple6) -> (rule8 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((((triple7) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
((triple10) -> (rule6 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((((triple10) -> (rule6 % int2))) -> (rule2 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((((triple10) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3