Bob is cold. Dave is round. Fiona is smart. Smart things are round. All quiet, big things are cold. If something is cold and round then it is big. If Bob is big and Bob is round then Bob is young. All round things are cold. Quiet things are young.
Bob is cold.
("Bob" "is" "cold" "+")
Dave is round.
("Dave" "is" "round" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Smart things are round.
((("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
All quiet, big things are cold.
((("something" "is" "quiet" "+") ("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
If something is cold and round then it is big.
((("something" "is" "cold" "+") ("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
If Bob is big and Bob is round then Bob is young.
((("Bob" "is" "big" "+") ("Bob" "is" "round" "+")) -> ("Bob" "is" "young" "+"))
All round things are cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
Quiet things are young.
((("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
Dave is round.
True
1
proof
[(triple2)]
("Dave" "is" "round" "+")
triple2
Bob is not cold.
False
1
inv-proof
[(triple1)]
("Bob" "is" "cold" "-")
triple1
Dave is cold.
True
2
proof
[(((triple2) -> rule5))]
("Dave" "is" "cold" "+")
((triple2) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Fiona is not round.
False
2
inv-proof
[(((triple3) -> rule1))]
("Fiona" "is" "round" "-")
((triple3) -> (rule1 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is cold.
True
3
proof
[(((((triple3) -> rule1)) -> rule5))]
("Fiona" "is" "cold" "+")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is not cold.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule5))]
("Fiona" "is" "cold" "-")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is big.
True
6
proof
[(((((((triple3) -> rule1)) -> rule5) ((triple3) -> rule1)) -> rule3))]
("Fiona" "is" "big" "+")
((((((triple3) -> (rule1 % int3))) -> (rule5 % int2)) ((triple3) -> (rule1 % int3))) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is not big.
False
6
inv-proof
[(((((((triple3) -> rule1)) -> rule5) ((triple3) -> rule1)) -> rule3))]
("Fiona" "is" "big" "-")
((((((triple3) -> (rule1 % int3))) -> (rule5 % int2)) ((triple3) -> (rule1 % int3))) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is not young.
Unknown
inv-rconc
[@1: Fiona is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "young" "-")
Bob is young.
Unknown
rconc
[@2: Bob is young.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Bob" "is" "young" "+")
Dave is not young.
Unknown
inv-rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "young" "-")
Bob is big.
Unknown
rconc
[@2: Bob is big.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Bob" "is" "big" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
Fiona is not rough.
Unknown
inv-random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
@0: Bob is cold.[(triple1)] Dave is round.[(triple2)] Fiona is smart.[(triple3)] @1: Dave is cold.[(((triple2) -> rule5))] Fiona is round.[(((triple3) -> rule1))] @2: Dave is big.[(((((triple2) -> rule5) triple2) -> rule3))] Fiona is cold.[(((((triple3) -> rule1)) -> rule5))] @3: Fiona is big.[(((((((triple3) -> rule1)) -> rule5) ((triple3) -> rule1)) -> rule3))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Dave is round.
("Dave" "is" "round" "+")
triple2
Fiona is smart.
("Fiona" "is" "smart" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
((triple2) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
((triple3) -> (rule1 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((((triple2) -> (rule5 % int2)) triple2) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
((((((triple3) -> (rule1 % int3))) -> (rule5 % int2)) ((triple3) -> (rule1 % int3))) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3