Charlie is big. Fiona is young. Harry is smart. If Harry is big then Harry is smart. Big things are young. If something is smart and young then it is nice. If something is rough then it is nice. All big, cold things are young. If something is nice and rough then it is cold. All cold, quiet things are smart. If something is smart then it is big.
Charlie is big.
("Charlie" "is" "big" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Harry is big then Harry is smart.
((("Harry" "is" "big" "+")) -> ("Harry" "is" "smart" "+"))
Big things are young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
If something is smart and young then it is nice.
((("something" "is" "smart" "+") ("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
If something is rough then it is nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
All big, cold things are young.
((("something" "is" "big" "+") ("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
If something is nice and rough then it is cold.
((("something" "is" "nice" "+") ("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
All cold, quiet things are smart.
((("something" "is" "cold" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
If something is smart then it is big.
((("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
Harry is smart.
True
1
proof
[(triple3)]
("Harry" "is" "smart" "+")
triple3
Fiona is not young.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "young" "-")
triple2
Harry is big.
True
2
proof
[(((triple3) -> rule8))]
("Harry" "is" "big" "+")
((triple3) -> (rule8 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Charlie is not young.
False
2
inv-proof
[(((triple1) -> rule2))]
("Charlie" "is" "young" "-")
((triple1) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Harry is young.
True
3
proof
[(((((triple3) -> rule8)) -> rule2))]
("Harry" "is" "young" "+")
((((triple3) -> (rule8 % int2))) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not young.
False
3
inv-proof
[(((((triple3) -> rule8)) -> rule2))]
("Harry" "is" "young" "-")
((((triple3) -> (rule8 % int2))) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is nice.
True
5
proof
[(((triple3 ((((triple3) -> rule8)) -> rule2)) -> rule3))]
("Harry" "is" "nice" "+")
((triple3 ((((triple3) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is not nice.
False
5
inv-proof
[(((triple3 ((((triple3) -> rule8)) -> rule2)) -> rule3))]
("Harry" "is" "nice" "-")
((triple3 ((((triple3) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Charlie is not smart.
Unknown
inv-rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "smart" "-")
Fiona is big.
Unknown
rconc
[@2: Fiona is big.[CWA. Example of deepest failure = (rule8 <- rule7 <- FAIL)]]
("Fiona" "is" "big" "+")
Charlie is not nice.
Unknown
inv-rconc
[@2: Charlie is nice.[CWA. Example of deepest failure = (rule3 <- rule7 <- FAIL)]]
("Charlie" "is" "nice" "-")
Fiona is nice.
Unknown
rconc
[@2: Fiona is nice.[CWA. Example of deepest failure = (rule3 <- rule7 <- FAIL)]]
("Fiona" "is" "nice" "+")
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Charlie is big.[(triple1)] Fiona is young.[(triple2)] Harry is smart.[(triple3)] @1: Charlie is young.[(((triple1) -> rule2))] Harry is big.[(((triple3) -> rule8))] @2: Harry is young.[(((((triple3) -> rule8)) -> rule2))] @3: Harry is nice.[(((triple3 ((((triple3) -> rule8)) -> rule2)) -> rule3))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Fiona is young.
("Fiona" "is" "young" "+")
triple2
Harry is smart.
("Harry" "is" "smart" "+")
triple3
Charlie is young.
("Charlie" "is" "young" "+")
((triple1) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple3) -> (rule8 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((((triple3) -> (rule8 % int2))) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((triple3 ((((triple3) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3